1 /-
2 Copyright (c) 2017 Microsoft Corporation. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Author: Mario Carneiro
5
6 Coinductive formalization of unbounded computations.
7 -/
8 import data.stream logic.relator tactic.basic
src └─────────┘ └───────────┘ └──────────┘
9 universes u v w
10
11 /-
12 coinductive computation (α : Type u) : Type u
13 | return : α → computation α
14 | think : computation α → computation α
15 -/
16
17 /-- `computation α` is the type of unbounded computations returning `α`.
18 An element of `computation α` is an infinite sequence of `option α` such
19 that if `f n = some a` for some `n` then it is constantly `some a` after that. -/
20 def computation (α : Type u) : Type u :=
21 { f : stream (option α) // ∀ {n a}, f n = some a → f (n+1) = some a }
id ┴ └────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴┴ ┴ └──┘ ┴
src ┴ └────┘ └────┘ ┴ └──┘ ┴ ┴ └──┘
typ ┴ └────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴┴ ┴ └──┘ ┴
22
23 namespace computation
24 variables {α : Type u} {β : Type v} {γ : Type w}
id ┴
typ ┴
25
26 -- constructors
27 /-- `return a` is the computation that immediately terminates with result `a`. -/
28 def return (a : α) : computation α := ⟨stream.const (some a), λn a', id⟩
id ┴ └─────────┘ ┴ └──────────┘ └──┘ ┴ ┴ └┘ └┘
src └─────────┘ └──────────┘ └──┘ └┘
typ ┴ └─────────┘ ┴ └──────────┘ └──┘ ┴ ┴ └┘ └┘
doc └─────────┘
29
30 instance : has_coe_t α (computation α) := ⟨return⟩ -- note [use has_coe_t]
id └───────┘ ┴ └─────────┘ ┴ └────┘
src └───────┘ └─────────┘ └────┘
typ └───────┘ ┴ └─────────┘ ┴ └────┘
doc └───────┘ └─────────┘ └────┘
31
32 /-- `think c` is the computation that delays for one "tick" and then performs
33 computation `c`. -/
34 def think (c : computation α) : computation α :=
id └─────────┘ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ └─────────┘ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
35 ⟨none :: c.1, λn a h, by {cases n with n, contradiction, exact c.2 h}⟩
id └──┘ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ └┘ ┴ └────┘ └─────┘ └───────────┘ └────┘ └─┘
typ └──┘ └┘ ┴┴ ┴ ┴ ┴ └────┘┴└─────┘ └───────────┘ └────┘┴└─┘┴
doc └────┘ └─────┘ └───────────┘ └────┘ └─┘
txt └────┘ └─────┘ └───────────┘ └────┘ └─┘
par └────┘ └─────┘ └───────────┘ └────┘ └─┘
pid ┴ └─────┘ ┴ └─┘
st └──────────────┘└─────────────┘└───────────┘└┘
36
37 /-- `thinkN c n` is the computation that delays for `n` ticks and then performs
38 computation `c`. -/
39 def thinkN (c : computation α) : ℕ → computation α
id └─────────┘ ┴ ┴ ┴ └─────────┘ ┴
src └─────────┘ ┴ └─────────┘
typ └─────────┘ ┴ ┴ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
40 | 0 := c
id ┴
typ ┴
41 | (n+1) := think (thinkN n)
id ┴┴ └───┘ └────┘
src ┴ └───┘
typ ┴┴ └───┘ └────┘
doc └───┘
42
43 -- check for immediate result
44 /-- `head c` is the first step of computation, either `some a` if `c = return a`
45 or `none` if `c = think c'`. -/
46 def head (c : computation α) : option α := c.1.head
id └─────────┘ ┴ └────┘ ┴ ┴┴ └──┘
src └─────────┘ └────┘ ┴ └──┘
typ └─────────┘ ┴ └────┘ ┴ ┴┴ └──┘
doc └─────────┘
47
48 -- one step of computation
49 /-- `tail c` is the remainder of computation, either `c` if `c = return a`
50 or `c'` if `c = think c'`. -/
51 def tail (c : computation α) : computation α :=
id └─────────┘ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ └─────────┘ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
52 ⟨c.1.tail, λ n a, let t := c.2 in t⟩
id ┴┴ └──┘ ┴ ┴ ┴ ┴┴ ┴
src ┴ └──┘ ┴
typ ┴┴ └──┘ ┴ ┴ ┴ ┴┴ ┴
53
54 /-- `empty α` is the computation that never returns, an infinite sequence of
55 `think`s. -/
56 def empty (α) : computation α := ⟨stream.const none, λn a', id⟩
id └─────────┘ ┴ └──────────┘ └──┘ ┴ └┘ └┘
src └─────────┘ └──────────┘ └──┘ └┘
typ └─────────┘ ┴ └──────────┘ └──┘ ┴ └┘ └┘
doc └─────────┘
57
58 instance : inhabited (computation α) := ⟨empty _⟩
id └───────┘ └─────────┘ ┴ └───┘
src └───────┘ └─────────┘ └───┘
typ └───────┘ └─────────┘ ┴ └───┘
doc └─────────┘ └───┘
59
60 /-- `run_for c n` evaluates `c` for `n` steps and returns the result, or `none`
61 if it did not terminate after `n` steps. -/
62 def run_for : computation α → ℕ → option α := subtype.val
id └─────────┘ ┴ ┴ └────┘ ┴ └─────────┘
src └─────────┘ ┴ └────┘ └─────────┘
typ └─────────┘ ┴ ┴ └────┘ ┴ └─────────┘
doc └─────────┘
63
64 /-- `destruct c` is the destructor for `computation α` as a coinductive type.
65 It returns `inl a` if `c = return a` and `inr c'` if `c = think c'`. -/
66 def destruct (c : computation α) : α ⊕ computation α :=
id └─────────┘ ┴ ┴ ┴ └─────────┘ ┴
src └─────────┘ ┴ └─────────┘
typ └─────────┘ ┴ ┴ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
67 match c.1 0 with
id ┴┴
src ┴
typ ┴┴
68 | none := sum.inr (tail c)
id └──┘ └─────┘ └──┘ ┴
src └──┘ └─────┘ └──┘
typ └──┘ └─────┘ └──┘ ┴
doc └──┘
69 | some a := sum.inl a
id └──┘ ┴ └─────┘
src └──┘ └─────┘
typ └──┘ ┴ └─────┘
70 end
71
72 /-- `run c` is an unsound meta function that runs `c` to completion, possibly
73 resulting in an infinite loop in the VM. -/
74 meta def run : computation α → α | c :=
id └─────────┘ ┴ ┴ ┴ ┴
src └─────────┘
typ └─────────┘ ┴ ┴ ┴ ┴
doc └─────────┘
75 match destruct c with
id └──────┘
src └──────┘
typ └──────┘
doc └──────┘
76 | sum.inl a := a
id └─────┘ ┴
src └─────┘
typ └─────┘ ┴
77 | sum.inr ca := run ca
id └─────┘ └┘ └─┘
src └─────┘
typ └─────┘ └┘ └─┘
78 end
79
80 theorem destruct_eq_ret {s : computation α} {a : α} :
id └─────────┘ ┴ ┴
src └─────────┘
typ └─────────┘ ┴ ┴
doc └─────────┘
81 destruct s = sum.inl a → s = return a :=
id └──────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ └────┘ ┴
src └──────┘ ┴ └─────┘ ┴ └────┘
typ └──────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ └────┘ ┴
doc └──────┘ └────┘
82 begin
st └─────
83 dsimp [destruct],
id └──────┘
src └─────┘└──────┘┴
typ └─────┘└──────┘┴
doc └─────┘└──────┘┴
txt └─────┘ ┴
par └─────┘ ┴
pid ┴┴ ┴
st ─────────────────┘└─
84 induction f0 : s.1 0; intro h,
id ┴
src └────────┘ └─┘ └──┘ └─────┘
typ └────────┘ └─┘┴└──┘ └─────┘
doc └────────┘ └─┘ └──┘ └─────┘
txt └────────┘ └─┘ └──┘ └─────┘
par └────────┘ └─┘ └──┘ └─────┘
pid ┴ └─┘ └─┘┴ └┘
st ──────────────────────────────┘└─
85 { contradiction },
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid ┴
st ───┘└────────────┘└┘└
86 { apply subtype.eq, funext n,
id └────────┘
src └────┘└────────┘ └──────┘
typ └────┘└────────┘ └──────┘
doc └────┘ └──────┘
txt └────┘ └──────┘
par └────┘ └──────┘
pid ┴ └┘
st ───────────────────┘└────────┘└─
87 induction n with n IH,
id ┴
src └────────┘ └────────┘
typ └────────┘┴└────────┘
doc └────────┘ └────────┘
txt └────────┘ └────────┘
par └────────┘ └────────┘
pid ┴ ┴└───────┘
st ────────────────────────┘└─
88 { injection h with h', rwa h' at f0 },
id ┴ └┘
src └────────┘ └──────┘ └──┘ └─────┘
typ └────────┘┴└──────┘ └──┘└┘└─────┘
doc └────────┘ └──────┘ └──┘ └─────┘
txt └────────┘ └──────┘ └──┘ └─────┘
par └────────┘ └──────┘ └──┘ └─────┘
pid ┴ └──────┘ ┴ └────┘┴
st ─────┘└─────────────────┘└─────────────┘└┘└
89 { exact s.2 IH } }
id ┴ └┘
src └────┘ └─┘ ┴
typ └────┘┴└─┘└┘┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ──────────────────┘└───
90 end
st ──┘
91
92 theorem destruct_eq_think {s : computation α} {s'} :
id └─────────┘ ┴
src └─────────┘
typ └─────────┘ ┴
doc └─────────┘
93 destruct s = sum.inr s' → s = think s' :=
id └──────┘ ┴ ┴ └─────┘ └┘ ┴ ┴ └───┘ └┘
src └──────┘ ┴ └─────┘ ┴ └───┘
typ └──────┘ ┴ ┴ └─────┘ └┘ ┴ ┴ └───┘ └┘
doc └──────┘ └───┘
94 begin
st └─────
95 dsimp [destruct],
id └──────┘
src └─────┘└──────┘┴
typ └─────┘└──────┘┴
doc └─────┘└──────┘┴
txt └─────┘ ┴
par └─────┘ ┴
pid ┴┴ ┴
st ─────────────────┘└─
96 induction f0 : s.1 0 with a'; intro h,
id ┴
src └────────┘ └─┘ └──────────┘ └─────┘
typ └────────┘ └─┘┴└──────────┘ └─────┘
doc └────────┘ └─┘ └──────────┘ └─────┘
txt └────────┘ └─┘ └──────────┘ └─────┘
par └────────┘ └─┘ └──────────┘ └─────┘
pid ┴ └─┘ └─┘└┘└─────┘ └┘
st ──────────────────────────────────────┘└─
97 { injection h with h', rw ←h',
id ┴ └┘
src └────────┘ └──────┘ └──┘
typ └────────┘┴└──────┘ └──┘└┘
doc └────────┘ └──────┘ └──┘
txt └────────┘ └──────┘ └──┘
par └────────┘ └──────┘ └──┘
pid ┴ └──────┘ └┘
st ───┘└─────────────────┘└──────┘└─
98 cases s with f al,
id ┴
src └────┘ └────────┘
typ └────┘┴└────────┘
doc └────┘ └────────┘
txt └────┘ └────────┘
par └────┘ └────────┘
pid ┴ └────────┘
st ────────────────────┘└─
99 apply subtype.eq, dsimp [think, tail],
id └────────┘ └───┘ └──┘
src └────┘└────────┘ └─────┘└───┘└┘└──┘┴
typ └────┘└────────┘ └─────┘└───┘└┘└──┘┴
doc └────┘ └─────┘└───┘└┘└──┘┴
txt └────┘ └─────┘ └┘ ┴
par └────┘ └─────┘ └┘ ┴
pid ┴ ┴┴ └┘ ┴
st ───────────────────┘└───────────────────┘└─
100 rw ←f0, exact (stream.eta f).symm },
id └┘ └────────┘ ┴
src └──┘ └────┘ └────────┘┴ └─────┘
typ └──┘└┘ └────┘ └────────┘┴┴└─────┘
doc └──┘ └────┘ ┴ └─────┘
txt └──┘ └────┘ ┴ └─────┘
par └──┘ └────┘ ┴ └─────┘
pid └┘ ┴ ┴ └───┘└┘
st ─────────┘└──────────────────────────┘└┘└
101 { contradiction }
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid ┴
st ─────────────────┘└─
102 end
st ──┘
103
104 @[simp] theorem destruct_ret (a : α) : destruct (return a) = sum.inl a := rfl
id ┴ └──────┘ └────┘ ┴ ┴ └─────┘ ┴ └─┘
src └──────┘ └────┘ ┴ └─────┘ └─┘
typ ┴ └──────┘ └────┘ ┴ ┴ └─────┘ ┴ └─┘
doc └──┘ └──────┘ └────┘
105
106 @[simp] theorem destruct_think : ∀ s : computation α, destruct (think s) = sum.inr s
id ┴ └─────────┘ ┴ └──────┘ └───┘ ┴ ┴ └─────┘ ┴
src └─────────┘ └──────┘ └───┘ ┴ └─────┘
typ ┴ └─────────┘ ┴ └──────┘ └───┘ ┴ ┴ └─────┘ ┴
doc └──┘ └─────────┘ └──────┘ └───┘
107 | ⟨f, al⟩ := rfl
id └─┘
src └─┘
typ └─┘
108
109 @[simp] theorem destruct_empty : destruct (empty α) = sum.inr (empty α) := rfl
id └──────┘ └───┘ ┴ ┴ └─────┘ └───┘ ┴ └─┘
src └──────┘ └───┘ ┴ └─────┘ └───┘ └─┘
typ └──────┘ └───┘ ┴ ┴ └─────┘ └───┘ ┴ └─┘
doc └──┘ └──────┘ └───┘ └───┘
110
111 @[simp] theorem head_ret (a : α) : head (return a) = some a := rfl
id ┴ └──┘ └────┘ ┴ ┴ └──┘ ┴ └─┘
src └──┘ └────┘ ┴ └──┘ └─┘
typ ┴ └──┘ └────┘ ┴ ┴ └──┘ ┴ └─┘
doc └──┘ └──┘ └────┘
112
113 @[simp] theorem head_think (s : computation α) : head (think s) = none := rfl
id └─────────┘ ┴ └──┘ └───┘ ┴ ┴ └──┘ └─┘
src └─────────┘ └──┘ └───┘ ┴ └──┘ └─┘
typ └─────────┘ ┴ └──┘ └───┘ ┴ ┴ └──┘ └─┘
doc └──┘ └─────────┘ └──┘ └───┘
114
115 @[simp] theorem head_empty : head (empty α) = none := rfl
id └──┘ └───┘ ┴ ┴ └──┘ └─┘
src └──┘ └───┘ ┴ └──┘ └─┘
typ └──┘ └───┘ ┴ ┴ └──┘ └─┘
doc └──┘ └──┘ └───┘
116
117 @[simp] theorem tail_ret (a : α) : tail (return a) = return a := rfl
id ┴ └──┘ └────┘ ┴ ┴ └────┘ ┴ └─┘
src └──┘ └────┘ ┴ └────┘ └─┘
typ ┴ └──┘ └────┘ ┴ ┴ └────┘ ┴ └─┘
doc └──┘ └──┘ └────┘ └────┘
118
119 @[simp] theorem tail_think (s : computation α) : tail (think s) = s :=
id └─────────┘ ┴ └──┘ └───┘ ┴ ┴ ┴
src └─────────┘ └──┘ └───┘ ┴
typ └─────────┘ ┴ └──┘ └───┘ ┴ ┴ ┴
doc └──┘ └─────────┘ └──┘ └───┘
120 by cases s with f al; apply subtype.eq; dsimp [tail, think]; rw [stream.tail_cons]
id ┴ └────────┘ └──┘ └───┘ └──────────────┘
src └────┘ └────────┘ └────┘└────────┘ └─────┘└──┘└┘└───┘┴ └──┘└──────────────┘└─
typ └────┘┴└────────┘ └────┘└────────┘ └─────┘└──┘└┘└───┘┴ └──┘└──────────────┘└─
doc └────┘ └────────┘ └────┘ └─────┘└──┘└┘└───┘┴ └──┘ └─
txt └────┘ └────────┘ └────┘ └─────┘ └┘ ┴ └──┘ └─
par └────┘ └────────┘ └────┘ └─────┘ └┘ ┴ └──┘ └─
pid ┴ └────────┘ ┴ ┴┴ └┘ ┴ └┘ ┴└
st └─────────────────────────────────────────────────────────────┘└──────────────┘┴└
121
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
122 @[simp] theorem tail_empty : tail (empty α) = empty α := rfl
id └──┘ └───┘ ┴ ┴ └───┘ ┴ └─┘
src └──┘ └───┘ ┴ └───┘ └─┘
typ └──┘ └───┘ ┴ ┴ └───┘ ┴ └─┘
doc └──┘ └──┘ └───┘ └───┘
123
124 theorem think_empty : empty α = think (empty α) :=
id └───┘ ┴ ┴ └───┘ └───┘ ┴
src └───┘ ┴ └───┘ └───┘
typ └───┘ ┴ ┴ └───┘ └───┘ ┴
doc └───┘ └───┘ └───┘
125 destruct_eq_think destruct_empty
id └───────────────┘ └────────────┘
src └───────────────┘ └────────────┘
typ └───────────────┘ └────────────┘
126
127 def cases_on {C : computation α → Sort v} (s : computation α)
id └─────────┘ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ └─────────┘ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
128 (h1 : ∀ a, C (return a)) (h2 : ∀ s, C (think s)) : C s := begin
id ┴ ┴ └────┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
src └────┘ └───┘
typ ┴ ┴ └────┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
doc └────┘ └───┘
st └─────
129 induction H : destruct s with v v,
id └──────┘ ┴
src └────────┘ └─┘└──────┘┴ └───────┘
typ └────────┘ └─┘└──────┘┴┴└───────┘
doc └────────┘ └─┘└──────┘┴ └───────┘
txt └────────┘ └─┘ ┴ └───────┘
par └────────┘ └─┘ ┴ └───────┘
pid ┴ └─┘ ┴ ┴└──────┘
st ──────────────────────────────────┘└─
130 { rw destruct_eq_ret H, apply h1 },
id └─────────────┘ ┴
src └─┘└─────────────┘┴ └────┘ ┴
typ └─┘└─────────────┘┴┴ └────┘ ┴
doc └─┘ ┴ └────┘ ┴
txt └─┘ ┴ └────┘ ┴
par └─┘ ┴ └────┘ ┴
pid ┴ ┴ ┴ ┴
st ───┘└──────────────────┘└─────────┘└┘└
131 { cases v with a s', rw destruct_eq_think H, apply h2 }
id ┴ └───────────────┘ ┴
src └────┘ └────────┘ └─┘└───────────────┘┴ └────┘ ┴
typ └────┘┴└────────┘ └─┘└───────────────┘┴┴ └────┘ ┴
doc └────┘ └────────┘ └─┘ ┴ └────┘ ┴
txt └────┘ └────────┘ └─┘ ┴ └────┘ ┴
par └────┘ └────────┘ └─┘ ┴ └────┘ ┴
pid ┴ └────────┘ ┴ ┴ ┴ ┴
st ────────────────────┘└──────────────────────┘└─────────┘└─
132 end
st ──┘
133
134 def corec.F (f : β → α ⊕ β) : α ⊕ β → option α × (α ⊕ β)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └────┘ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
135 | (sum.inl a) := (some a, sum.inl a)
id └─────┘ ┴ ┴└──┘ └─────┘
src └─────┘ ┴└──┘ └─────┘
typ └─────┘ ┴ ┴└──┘ └─────┘
136 | (sum.inr b) := (match f b with
id └─────┘ ┴ ┴ ┴
src └─────┘ ┴
typ └─────┘ ┴ ┴ ┴
137 | sum.inl a := some a
id └─────┘ ┴ └──┘
src └─────┘ └──┘
typ └─────┘ ┴ └──┘
138 | sum.inr b' := none
id └─────┘ └──┘
src └─────┘ └──┘
typ └─────┘ └──┘
139 end, f b)
id ┴
typ ┴
140
141 /-- `corec f b` is the corecursor for `computation α` as a coinductive type.
142 If `f b = inl a` then `corec f b = return a`, and if `f b = inl b'` then
143 `corec f b = think (corec f b')`. -/
144 def corec (f : β → α ⊕ β) (b : β) : computation α :=
id ┴ ┴ ┴ ┴ ┴ └─────────┘ ┴
src ┴ └─────────┘
typ ┴ ┴ ┴ ┴ ┴ └─────────┘ ┴
doc └─────────┘
145 begin
st └─────
146 refine ⟨stream.corec' (corec.F f) (sum.inr b), λn a' h, _⟩,
id └───────────┘ └─────┘ ┴ └─────┘ ┴
src └─────┘ └───────────┘┴ └─────┘┴ └┘ └─────┘┴ └─┘ └────────┘
typ └─────┘ └───────────┘┴ └─────┘┴┴└┘ └─────┘┴┴└─┘ └────────┘
doc └─────┘ ┴ ┴ └┘ ┴ └─┘ └────────┘
txt └─────┘ ┴ ┴ └┘ ┴ └─┘ └────────┘
par └─────┘ ┴ ┴ └┘ ┴ └─┘ └────────┘
pid ┴ ┴ ┴ └┘ ┴ └─┘ └────────┘
st ───────────────────────────────────────────────────────────┘└─
147 rw stream.corec'_eq,
id └──────────────┘
src └─┘└──────────────┘
typ └─┘└──────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────────────────┘└─
148 change stream.corec' (corec.F f) (corec.F f (sum.inr b)).2 n = some a',
id └───────────┘ └─────┘ ┴ └─────┘ ┴ ┴ ┴ └──┘ └┘
src └─────┘└───────────┘┴ ┴ └┘ └─────┘┴ ┴ └─────┘┴ └───┘ ┴┴┴└──┘┴
typ └─────┘└───────────┘┴ ┴ └┘ └─────┘┴┴┴ └─────┘┴┴└───┘┴┴┴┴└──┘┴└┘
doc └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
txt └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
par └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
pid ┴ ┴ ┴ └┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────────────┘└─
149 revert h, generalize : sum.inr b = o, revert o,
id └─────┘ ┴
src └──────┘ └───────────┘└─────┘┴ ┴ ┴ └──────┘
typ └──────┘ └───────────┘└─────┘┴┴┴ ┴ └──────┘
doc └──────┘ └───────────┘ ┴ ┴ ┴ └──────┘
txt └──────┘ └───────────┘ ┴ ┴ ┴ └──────┘
par └──────┘ └───────────┘ ┴ ┴ ┴ └──────┘
pid └┘ ┴┴┴ ┴ ┴ ┴ └┘
st ─────────┘└──────────────────────────┘└────────┘└─
150 induction n with n IH; intro o,
id ┴
src └────────┘ └────────┘ └─────┘
typ └────────┘┴└────────┘ └─────┘
doc └────────┘ └────────┘ └─────┘
txt └────────┘ └────────┘ └─────┘
par └────────┘ └────────┘ └─────┘
pid ┴ ┴└───────┘ └┘
st ───────────────────────────────┘└─
151 { change (corec.F f o).1 = some a' → (corec.F f (corec.F f o).2).1 = some a',
id ┴ └─────┘ ┴ ┴ └──┘ └┘
src └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘┴ ┴ └─────┘ ┴└──┘┴
typ └─────┘ ┴ ┴ └──┘┴┴ ┴ ┴ ┴ ┴ ┴ └─────┘┴┴┴┴└─────┘ ┴└──┘┴└┘
doc └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴
txt └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴
par └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴
pid ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴
st ───┘└────────────────────────────────────────────────────────────────────────┘└─
152 cases o with a b; intro h, { exact h },
id ┴ ┴
src └────┘ └───────┘ └─────┘ └────┘ ┴
typ └────┘┴└───────┘ └─────┘ └────┘┴┴
doc └────┘ └───────┘ └─────┘ └────┘ ┴
txt └────┘ └───────┘ └─────┘ └────┘ ┴
par └────┘ └───────┘ └─────┘ └────┘ ┴
pid ┴ └───────┘ └┘ ┴ ┴
st ────────────────────────────┘└──┘└──────┘└┘└
153 dsimp [corec.F] at h, dsimp [corec.F],
id └─────┘ └─────┘
src └─────┘└─────┘└────┘ └─────┘└─────┘┴
typ └─────┘└─────┘└────┘ └─────┘└─────┘┴
doc └─────┘ └────┘ └─────┘ ┴
txt └─────┘ └────┘ └─────┘ ┴
par └─────┘ └────┘ └─────┘ ┴
pid ┴┴ ┴┴└──┘ ┴┴ ┴
st ───────────────────────┘└───────────────┘└─
154 cases f b with a b', { exact h },
id ┴ ┴ ┴
src └────┘ ┴ └────────┘ └────┘ ┴
typ └────┘┴┴┴└────────┘ └────┘┴┴
doc └────┘ ┴ └────────┘ └────┘ ┴
txt └────┘ ┴ └────────┘ └────┘ ┴
par └────┘ ┴ └────────┘ └────┘ ┴
pid ┴ ┴ └────────┘ ┴ ┴
st ──────────────────────┘└──┘└──────┘└┘└
155 { contradiction } },
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid ┴
st ───────────────────┘└──┘└
156 { rw [stream.corec'_eq (corec.F f) (corec.F f o).2,
id └──────────────┘ └─────┘ ┴ ┴
src └──┘└──────────────┘┴ ┴ └┘ └─────┘┴ ┴ └────
typ └──┘└──────────────┘┴ ┴ └┘ └─────┘┴┴┴┴└────
doc └──┘ ┴ ┴ └┘ ┴ ┴ └────
txt └──┘ ┴ ┴ └┘ ┴ ┴ └────
par └──┘ ┴ ┴ └┘ ┴ ┴ └────
pid └┘ ┴ ┴ └┘ ┴ ┴ └────
st ─────────────────────────────────────────────────┘└───
157 stream.corec'_eq (corec.F f) o],
id └──────────────┘ └─────┘ ┴ ┴
src ───────┘└──────────────┘┴ └─────┘┴ └┘ ┴
typ ───────┘└──────────────┘┴ └─────┘┴┴└┘┴┴
doc ───────┘ ┴ ┴ └┘ ┴
txt ───────┘ ┴ ┴ └┘ ┴
par ───────┘ ┴ ┴ └┘ ┴
pid ───────┘ ┴ ┴ └┘ ┴
st ─────────────────────────────────────┘┴└─
158 exact IH (corec.F f o).2 }
id └┘ └─────┘ ┴ ┴
src └────┘ ┴ └─────┘┴ ┴ └──┘
typ └────┘└┘┴ └─────┘┴┴┴┴└──┘
doc └────┘ ┴ ┴ ┴ └──┘
txt └────┘ ┴ ┴ ┴ └──┘
par └────┘ ┴ ┴ ┴ └──┘
pid ┴ ┴ ┴ ┴ ┴└─┘
st ────────────────────────────┘└─
159 end
st ──┘
160
161 /-- left map of `⊕` -/
162 def lmap (f : α → β) : α ⊕ γ → β ⊕ γ
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
163 | (sum.inl a) := sum.inl (f a)
id └─────┘ ┴ └─────┘ ┴
src └─────┘ └─────┘
typ └─────┘ ┴ └─────┘ ┴
164 | (sum.inr b) := sum.inr b
id └─────┘ ┴ └─────┘
src └─────┘ └─────┘
typ └─────┘ ┴ └─────┘
165
166 /-- right map of `⊕` -/
167 def rmap (f : β → γ) : α ⊕ β → α ⊕ γ
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
168 | (sum.inl a) := sum.inl a
id └─────┘ ┴ └─────┘
src └─────┘ └─────┘
typ └─────┘ ┴ └─────┘
169 | (sum.inr b) := sum.inr (f b)
id └─────┘ ┴ └─────┘ ┴
src └─────┘ └─────┘
typ └─────┘ ┴ └─────┘ ┴
170 attribute [simp] lmap rmap
id └──┘ └──┘
src └──┘ └──┘
typ └──┘ └──┘
doc └──┘ └──┘ └──┘
171
172 @[simp] lemma corec_eq (f : β → α ⊕ β) (b : β) :
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
doc └──┘
173 destruct (corec f b) = rmap (corec f) (f b) :=
id └──────┘ └───┘ ┴ ┴ ┴ └──┘ └───┘ ┴ ┴ ┴
src └──────┘ └───┘ ┴ └──┘ └───┘
typ └──────┘ └───┘ ┴ ┴ ┴ └──┘ └───┘ ┴ ┴ ┴
doc └──────┘ └───┘ └──┘ └───┘
174 begin
st └─────
175 dsimp [corec, destruct],
id └───┘ └──────┘
src └─────┘└───┘└┘└──────┘┴
typ └─────┘└───┘└┘└──────┘┴
doc └─────┘└───┘└┘└──────┘┴
txt └─────┘ └┘ ┴
par └─────┘ └┘ ┴
pid ┴┴ └┘ ┴
st ────────────────────────┘└─
176 change stream.corec' (corec.F f) (sum.inr b) 0 with corec.F._match_1 (f b),
id └───────────┘ └─────┘ ┴ └─────┘ ┴ └──────────────┘ ┴ ┴
src └─────┘└───────────┘┴ └─────┘┴ └┘ └─────┘┴ └───────┘└──────────────┘┴ ┴ ┴
typ └─────┘└───────────┘┴ └─────┘┴┴└┘ └─────┘┴┴└───────┘└──────────────┘┴ ┴┴┴┴
doc └─────┘ ┴ ┴ └┘ ┴ └───────┘ ┴ ┴ ┴
txt └─────┘ ┴ ┴ └┘ ┴ └───────┘ ┴ ┴ ┴
par └─────┘ ┴ ┴ └┘ ┴ └───────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ └┘ ┴ └┘└─────┘ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────────────────┘└─
177 induction h : f b with a b', { refl },
id ┴ ┴
src └────────┘ └─┘ ┴ └────────┘ └───┘
typ └────────┘ └─┘┴┴┴└────────┘ └───┘
doc └────────┘ └─┘ ┴ └────────┘ └───┘
txt └────────┘ └─┘ ┴ └────────┘ └───┘
par └────────┘ └─┘ ┴ └────────┘ └───┘
pid ┴ └─┘ ┴ ┴└───────┘ ┴
st ────────────────────────────┘└──┘└───┘└┘└
178 dsimp [corec.F, destruct],
id └─────┘ └──────┘
src └─────┘└─────┘└┘└──────┘┴
typ └─────┘└─────┘└┘└──────┘┴
doc └─────┘ └┘└──────┘┴
txt └─────┘ └┘ ┴
par └─────┘ └┘ ┴
pid ┴┴ └┘ ┴
st ──────────────────────────┘└─
179 apply congr_arg, apply subtype.eq,
id └───────┘ └────────┘
src └────┘└───────┘ └────┘└────────┘
typ └────┘└───────┘ └────┘└────────┘
doc └────┘ └────┘
txt └────┘ └────┘
par └────┘ └────┘
pid ┴ ┴
st ────────────────┘└────────────────┘└─
180 dsimp [corec, tail],
id └───┘ └──┘
src └─────┘└───┘└┘└──┘┴
typ └─────┘└───┘└┘└──┘┴
doc └─────┘└───┘└┘└──┘┴
txt └─────┘ └┘ ┴
par └─────┘ └┘ ┴
pid ┴┴ └┘ ┴
st ────────────────────┘└─
181 rw [stream.corec'_eq, stream.tail_cons],
id └──────────────┘ └──────────────┘
src └──┘└──────────────┘└┘└──────────────┘┴
typ └──┘└──────────────┘└┘└──────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ─────────────────────┘└────────────────┘└──
182 dsimp [corec.F], rw h
id └─────┘ ┴
src └─────┘└─────┘┴ └─┘ ┴
typ └─────┘└─────┘┴ └─┘┴┴
doc └─────┘ ┴ └─┘ ┴
txt └─────┘ ┴ └─┘ ┴
par └─────┘ ┴ └─┘ ┴
pid ┴┴ ┴ ┴ ┴
st ────────────────┘└─────┘
183 end
st └─┘
184
185 section bisim
186 variable (R : computation α → computation α → Prop)
id └─────────┘ └─────────┘
src └─────────┘ └─────────┘
typ └─────────┘ └─────────┘
doc └─────────┘ └─────────┘
187
188 local infix ~ := R
189
190 def bisim_o : α ⊕ computation α → α ⊕ computation α → Prop
id ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ └─────────┘ ┴
src ┴ └─────────┘ ┴ └─────────┘
typ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
191 | (sum.inl a) (sum.inl a') := a = a'
id ┴ └─────┘ └┘ ┴
src └─────┘ ┴
typ ┴ └─────┘ └┘ ┴
192 | (sum.inr s) (sum.inr s') := R s s'
id ┴ └─────┘ └┘ ┴
src └─────┘
typ ┴ └─────┘ └┘ ┴
193 | _ _ := false
id └───┘
src └───┘
typ └───┘
194 attribute [simp] bisim_o
id └─────┘
src └─────┘
typ └─────┘
doc └──┘
195
196 def is_bisimulation := ∀ ⦃s₁ s₂⦄, s₁ ~ s₂ → bisim_o R (destruct s₁) (destruct s₂)
id └┘ └┘ └┘ ┴ └┘ └─────┘ ┴ └──────┘ └┘ └──────┘ └┘
src └─────┘ └──────┘ └──────┘
typ └┘ └┘ └┘ ┴ └┘ └─────┘ ┴ └──────┘ └┘ └──────┘ └┘
doc └──────┘ └──────┘
197
198 -- If two computations are bisimilar, then they are equal
199 theorem eq_of_bisim (bisim : is_bisimulation R) {s₁ s₂} (r : s₁ ~ s₂) : s₁ = s₂ :=
id └─────────────┘ ┴ └┘ ┴ └┘ └┘ ┴ └┘
src └─────────────┘ ┴
typ └─────────────┘ ┴ └┘ ┴ └┘ └┘ ┴ └┘
200 begin
st └─────
201 apply subtype.eq,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────┘└─
202 apply stream.eq_of_bisim (λx y, ∃ s s' : computation α, s.1 = x ∧ s'.1 = y ∧ R s s'),
id └────────────────┘ ┴ └─────────┘ ┴┴ ┴ ┴ ┴
src └────┘└────────────────┘┴ └───┘┴└──────┘└─────────┘┴ ┴┴ └─┘┴┴ ┴┴┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └────┘└────────────────┘┴ └───┘┴└──────┘└─────────┘┴┴┴┴ └─┘┴┴ ┴┴┴ └─┘ ┴ ┴ ┴┴┴ ┴ ┴
doc └────┘ ┴ └───┘ └──────┘└─────────┘┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
txt └────┘ ┴ └───┘ └──────┘ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
par └────┘ ┴ └───┘ └──────┘ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ └───┘ └──────┘ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────────────────────────────┘└─
203 dsimp [stream.is_bisimulation],
id └────────────────────┘
src └─────┘└────────────────────┘┴
typ └─────┘└────────────────────┘┴
doc └─────┘ ┴
txt └─────┘ ┴
par └─────┘ ┴
pid ┴┴ ┴
st ─────────────────────────────────┘└─
204 intros t₁ t₂ e,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └──────┘
st ─────────────────┘└─
205 exact match t₁, t₂, e with ._, ._, ⟨s, s', rfl, rfl, r⟩ :=
id └┘ └┘ ┴ ┴ └┘ └─┘
src └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘└─┘└┘ └────
typ └────┘ ┴└┘└┘└┘└┘┴└────┘ └┘ └┘ ┴└┘└┘└┘ └┘└─┘└┘ └────
doc └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └┘ └────
txt └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └┘ └────
par └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └┘ └────
pid ┴ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └┘ └────
st ───────────────────────────────────────────────────────────────
206 suffices head s = head s' ∧ R (tail s) (tail s'), from
id └──┘ ┴
src ─────┘ └────┘ ┴ ┴└──┘┴ ┴ ┴ ┴ ┴ └┘ ┴ └───────
typ ─────┘ └────┘ ┴ ┴└──┘┴ ┴ ┴┴┴ ┴ └┘ ┴ └───────
doc ─────┘ └────┘ ┴ ┴└──┘┴ ┴ ┴ ┴ ┴ └┘ ┴ └───────
txt ─────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───────
par ─────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───────
pid ─────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───────
st ─────────────────────────────────────────────────────────────
207 and.imp id (λr, ⟨tail s, tail s',
id └─────┘ └┘ └──┘
src ─────┘└─────┘┴└┘┴ └─┘ ┴ └┘└──┘┴ └─
typ ─────┘└─────┘┴└┘┴ └─┘ ┴ └┘└──┘┴ └─
doc ─────┘ ┴ ┴ └─┘ ┴ └┘└──┘┴ └─
txt ─────┘ ┴ ┴ └─┘ ┴ └┘ ┴ └─
par ─────┘ ┴ ┴ └─┘ ┴ └┘ ┴ └─
pid ─────┘ ┴ ┴ └─┘ ┴ └┘ ┴ └─
st ────────────────────────────────────────
208 by cases s; refl, by cases s'; refl, r⟩) this,
id ┴ └┘
src ───────┘ ┴└────┘ └┘└──┘└┘ ┴└────┘ └┘└──┘└┘ └─┘ └─
typ ───────┘ ┴└────┘┴└┘└──┘└┘ ┴└────┘└┘└┘└──┘└┘ └─┘ └─
doc ───────┘ ┴└────┘ └┘└──┘└┘ ┴└────┘ └┘└──┘└┘ └─┘ └─
txt ───────┘ ┴└────┘ └┘└──┘└┘ ┴└────┘ └┘└──┘└┘ └─┘ └─
par ───────┘ ┴└────┘ └┘└──┘└┘ ┴└────┘ └┘└──┘└┘ └─┘ └─
pid ───────┘ └─────┘ └──────┘ └─────┘ └──────┘ └─┘ └─
st ─────────┘└────────────┘└──┘└─────────────┘└───────────
209 begin
src ─────┘ └
typ ─────┘ └
doc ─────┘ └
txt ─────┘ └
par ─────┘ └
pid ─────┘ └
st ─────┘└─────
210 have := bisim r, revert r this,
id └───┘ ┴
src ───────┘└──────┘ ┴ └┘└───────────┘└─
typ ───────┘└──────┘└───┘┴┴└┘└───────────┘└─
doc ───────┘└──────┘ ┴ └┘└───────────┘└─
txt ───────┘└──────┘ ┴ └┘└───────────┘└─
par ───────┘└──────┘ ┴ └┘└───────────┘└─
pid ───────────────┘ ┴ └────────────────
st ──────────────────────┘└─────────────┘└─
211 apply cases_on s _ _; intros; apply cases_on s' _ _; intros; intros r this,
id └──────┘ ┴ └──────┘ └┘
src ───────┘└────┘└──────┘┴ └──┘└┘└────┘└┘└────┘└──────┘┴ └──┘└┘└────┘└┘└───────────┘└─
typ ─────────────┘└──────┘┴┴└────┘└────┘└──────┘└──────┘┴└┘└────┘└────┘└┘└───────────┘└─
doc ───────┘└────┘ ┴ └──┘└┘└────┘└┘└────┘ ┴ └──┘└┘└────┘└┘└───────────┘└─
txt ───────┘└────┘ ┴ └──┘└┘└────┘└┘└────┘ ┴ └──┘└┘└────┘└┘└───────────┘└─
par ─────────────┘ ┴ └────┘└────┘└──────┘ ┴ └────┘└────┘└┘└───────────┘└─
pid ─────────────┘ ┴ └──────────────────┘ ┴ └────────────────────────────
st ─────────────────────────────────────────────────────────────────────────────────┘└─
212 { constructor, dsimp at this, rw this, assumption },
id └──┘
src ─────────┘└─────────┘└┘└───────────┘└┘└─┘ └┘└─────────┘└──
typ ─────────┘└─────────┘└┘└───────────┘└┘└─┘└──┘└┘└─────────┘└──
doc ─────────┘└─────────┘└┘└───────────┘└┘└─┘ └┘└─────────┘└──
txt ─────────┘└─────────┘└┘└───────────┘└┘└─┘ └┘└─────────┘└──
par ─────────┘└─────────┘└┘└───────────┘└┘└─┘ └┘└─────────┘└──
pid ────────────────────────────────────────┘ └───────────────
st ────────┘└──────────┘└─────────────┘└───────┘└───────────┘┴└─
213 { rw [destruct_ret, destruct_think] at this,
id └──────────┘ └────────────┘
src ─────────┘└──┘└──────────┘└┘└────────────┘└───────┘└─
typ ─────────┘└──┘└──────────┘└┘└────────────┘└───────┘└─
doc ─────────┘└──┘ └┘ └───────┘└─
txt ─────────┘└──┘ └┘ └───────┘└─
par ─────────┘└──┘ └┘ └───────┘└─
pid ─────────────┘ └┘ └──────────
st ────────┘└───────────────┘└──────────────┘┴└──────┘└─
214 exact false.elim this },
id └────────┘ └──┘
src ───────────────┘└────────┘┴ └───
typ ───────────────┘└────────┘┴└──┘└───
doc ───────────────┘ ┴ └───
txt ───────────────┘ ┴ └───
par ───────────────┘ ┴ └───
pid ───────────────┘ ┴ └───
st ───────────────────────────────┘┴└─
215 { rw [destruct_ret, destruct_think] at this,
id └──────────┘ └────────────┘
src ─────────┘└──┘└──────────┘└┘└────────────┘└───────┘└─
typ ─────────┘└──┘└──────────┘└┘└────────────┘└───────┘└─
doc ─────────┘└──┘ └┘ └───────┘└─
txt ─────────┘└──┘ └┘ └───────┘└─
par ─────────┘└──┘ └┘ └───────┘└─
pid ─────────────┘ └┘ └──────────
st ────────┘└───────────────┘└──────────────┘┴└──────┘└─
216 exact false.elim this },
id └────────┘ └──┘
src ───────────────┘└────────┘┴ └───
typ ───────────────┘└────────┘┴└──┘└───
doc ───────────────┘ ┴ └───
txt ───────────────┘ ┴ └───
par ───────────────┘ ┴ └───
pid ───────────────┘ ┴ └───
st ───────────────────────────────┘┴└─
217 { simp at this, simp [*] }
src ─────────┘└──────────┘└┘└───────┘└─
typ ─────────┘└──────────┘└┘└───────┘└─
doc ─────────┘└──────────┘└┘└───────┘└─
txt ─────────┘└──────────┘└┘└───────┘└─
par ─────────┘└──────────┘└┘└───────┘└─
pid ───────────────────────────────────
st ─────────────────────┘└─────────┘└─
218 end
src ──────────
typ ──────────
doc ──────────
txt ──────────
par ──────────
pid ──────────
st ────────┘└
219 end,
src ──────┘
typ ──────┘
doc ──────┘
txt ──────┘
par ──────┘
pid ──────┘
st ──────┘└─
220 exact ⟨s₁, s₂, rfl, rfl, r⟩
id └┘ └┘ └─┘ ┴
src └────┘ └┘ └┘ └┘└─┘└┘ └─
typ └────┘ └┘└┘└┘└┘ └┘└─┘└┘┴└─
doc └────┘ └┘ └┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └┘ └┘ └─
par └────┘ └┘ └┘ └┘ └┘ └─
pid ┴ └┘ └┘ └┘ └┘ ┴└
st ────────────────────────────────
221 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
222 end bisim
223
224 -- It's more of a stretch to use ∈ for this relation, but it
225 -- asserts that the computation limits to the given value.
226 protected def mem (a : α) (s : computation α) := some a ∈ s.1
id ┴ └─────────┘ ┴ └──┘ ┴ ┴ ┴┴
src └─────────┘ └──┘ ┴ ┴
typ ┴ └─────────┘ ┴ └──┘ ┴ ┴ ┴┴
doc └─────────┘
227
228 instance : has_mem α (computation α) := ⟨computation.mem⟩
id └─────┘ ┴ └─────────┘ ┴ └─────────────┘
src └─────┘ └─────────┘ └─────────────┘
typ └─────┘ ┴ └─────────┘ ┴ └─────────────┘
doc └─────────┘
229
230 theorem le_stable (s : computation α) {a m n} (h : m ≤ n) :
id └─────────┘ ┴ ┴ ┴ ┴
src └─────────┘ ┴
typ └─────────┘ ┴ ┴ ┴ ┴
doc └─────────┘
231 s.1 m = some a → s.1 n = some a :=
id ┴┴ ┴ ┴ └──┘ ┴ ┴┴ ┴ ┴ └──┘ ┴
src ┴ ┴ └──┘ ┴ ┴ └──┘
typ ┴┴ ┴ ┴ └──┘ ┴ ┴┴ ┴ ┴ └──┘ ┴
232 by {cases s with f al, induction h with n h IH, exacts [id, λ h2, al (IH h2)]}
id ┴ ┴ └┘ └┘ └┘
src └────┘ └────────┘ └────────┘ └──────────┘ └──────┘└┘└┘ └───┘ ┴ ┴ └┘
typ └────┘┴└────────┘ └────────┘┴└──────────┘ └──────┘└┘└┘ └───┘└┘┴ └┘┴ └┘
doc └────┘ └────────┘ └────────┘ └──────────┘ └──────┘ └┘ └───┘ ┴ ┴ └┘
txt └────┘ └────────┘ └────────┘ └──────────┘ └──────┘ └┘ └───┘ ┴ ┴ └┘
par └────┘ └────────┘ └────────┘ └──────────┘ └──────┘ └┘ └───┘ ┴ ┴ └┘
pid ┴ └────────┘ ┴ ┴└─────────┘ └┘ └┘ └───┘ ┴ ┴ └┘
st └─────────────────┘└───────────────────────┘└─────────────────────────────┘└┘
233
234 theorem mem_unique :
235 relator.left_unique ((∈) : α → computation α → Prop) :=
id └─────────────────┘ ┴ ┴ └─────────┘ ┴
src └─────────────────┘ ┴ └─────────┘
typ └─────────────────┘ ┴ ┴ └─────────┘ ┴
doc └─────────┘
236 λa s b ⟨m, ha⟩ ⟨n, hb⟩, by injection
id ┴ ┴ ┴ ┴ ┴
src └─────────
typ ┴ ┴ ┴ ┴ ┴ └─────────
doc └─────────
txt └─────────
par └─────────
pid └
st └──────────
237 (le_stable s (le_max_left m n) ha.symm).symm.trans
id └─────────┘ └─────┘
src ─┘ ┴ ┴ └─────────┘┴ ┴ └┘└─────┘└────────────
typ ─┘ ┴ ┴ └─────────┘┴ ┴ └┘└─────┘└────────────
doc ─┘ ┴ ┴ ┴ ┴ └┘ └────────────
txt ─┘ ┴ ┴ ┴ ┴ └┘ └────────────
par ─┘ ┴ ┴ ┴ ┴ └┘ └────────────
pid ─┘ ┴ ┴ ┴ ┴ └┘ └────────────
st ─────────────────────────────────────────────────────
238 (le_stable s (le_max_right m n) hb.symm)
id └───────┘ ┴ └──────────┘ ┴ ┴ └─────┘
src ─┘ └───────┘┴ ┴ └──────────┘┴ ┴ └┘└─────┘└─
typ ─┘ └───────┘┴┴┴ └──────────┘┴┴┴┴└┘└─────┘└─
doc ─┘ ┴ ┴ ┴ ┴ └┘ └─
txt ─┘ ┴ ┴ ┴ ┴ └┘ └─
par ─┘ ┴ ┴ ┴ ┴ └┘ └─
pid ─┘ ┴ ┴ ┴ ┴ └┘ ┴└
st ───────────────────────────────────────────
239
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
240 /-- `terminates s` asserts that the computation `s` eventually terminates with some value. -/
241 @[class] def terminates (s : computation α) : Prop := ∃ a, a ∈ s
id └─────────┘ ┴ ┴ ┴┴ ┴ ┴ ┴
src └─────────┘ ┴ ┴ ┴
typ └─────────┘ ┴ ┴ ┴┴ ┴ ┴ ┴
doc └─────────┘
242
243 theorem terminates_of_mem {s : computation α} {a : α} : a ∈ s → terminates s :=
id └─────────┘ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴
src └─────────┘ ┴ └────────┘
typ └─────────┘ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴
doc └─────────┘ └────────┘
244 exists.intro a
id └──────────┘ ┴
src └──────────┘
typ └──────────┘ ┴
245
246 theorem terminates_def (s : computation α) : terminates s ↔ ∃ n, (s.1 n).is_some :=
id └─────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴┴ ┴┴ ┴ └─────┘
src └─────────┘ └────────┘ ┴ ┴ ┴ ┴ └─────┘
typ └─────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴┴ ┴┴ ┴ └─────┘
doc └─────────┘ └────────┘
247 ⟨λ⟨a, n, h⟩, ⟨n, by {dsimp [stream.nth] at h, rw ←h, exact rfl}⟩,
id ┴ ┴ └────────┘ ┴ └─┘
src └─────┘└────────┘└────┘ └──┘ └────┘└─┘
typ ┴ ┴ └─────┘└────────┘└────┘ └──┘┴ └────┘└─┘
doc └─────┘ └────┘ └──┘ └────┘
txt └─────┘ └────┘ └──┘ └────┘
par └─────┘ └────┘ └──┘ └────┘
pid ┴┴ ┴┴└──┘ └┘ ┴
st └───────────────────────┘└─────┘└─────────┘└┘
248 λ⟨n, h⟩, ⟨option.get h, n, (option.eq_some_of_is_some h).symm⟩⟩
id ┴┴ ┴ └────────┘ └───────────────────────┘ └──┘
src └────────┘ └───────────────────────┘ └──┘
typ ┴┴ ┴ └────────┘ └───────────────────────┘ └──┘
249
250 theorem ret_mem (a : α) : a ∈ return a :=
id ┴ ┴ ┴ └────┘ ┴
src ┴ └────┘
typ ┴ ┴ ┴ └────┘ ┴
doc └────┘
251 exists.intro 0 rfl
id └──────────┘ └─┘
src └──────────┘ └─┘
typ └──────────┘ └─┘
252
253 theorem eq_of_ret_mem {a a' : α} (h : a' ∈ return a) : a' = a :=
id ┴ └┘ ┴ └────┘ ┴ └┘ ┴ ┴
src ┴ └────┘ ┴
typ ┴ └┘ ┴ └────┘ ┴ └┘ ┴ ┴
doc └────┘
254 mem_unique h (ret_mem _)
id └────────┘ ┴ └─────┘
src └────────┘ └─────┘
typ └────────┘ ┴ └─────┘
255
256 instance ret_terminates (a : α) : terminates (return a) :=
id ┴ └────────┘ └────┘ ┴
src └────────┘ └────┘
typ ┴ └────────┘ └────┘ ┴
doc └────────┘ └────┘
257 terminates_of_mem (ret_mem _)
id └───────────────┘ └─────┘
src └───────────────┘ └─────┘
typ └───────────────┘ └─────┘
258
259 theorem think_mem {s : computation α} {a} : a ∈ s → a ∈ think s
id └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴
src └─────────┘ ┴ ┴ └───┘
typ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴
doc └─────────┘ └───┘
260 | ⟨n, h⟩ := ⟨n+1, h⟩
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
261
262 instance think_terminates (s : computation α) :
id └─────────┘ ┴
src └─────────┘
typ └─────────┘ ┴
doc └─────────┘
263 ∀ [terminates s], terminates (think s)
id ┴└────────┘ ┴ └────────┘ └───┘ ┴
src └────────┘ └────────┘ └───┘
typ ┴└────────┘ ┴ └────────┘ └───┘ ┴
doc └────────┘ └────────┘ └───┘
264 | ⟨a, n, h⟩ := ⟨a, n+1, h⟩
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
265
266 theorem of_think_mem {s : computation α} {a} : a ∈ think s → a ∈ s
id └─────────┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
src └─────────┘ ┴ └───┘ ┴
typ └─────────┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
doc └─────────┘ └───┘
267 | ⟨n, h⟩ := by {cases n with n', contradiction, exact ⟨n', h⟩}
id ┴ └┘ ┴
src └────┘ └──────┘ └───────────┘ └────┘ └┘ ┴
typ └────┘┴└──────┘ └───────────┘ └────┘ └┘└┘┴┴
doc └────┘ └──────┘ └───────────┘ └────┘ └┘ ┴
txt └────┘ └──────┘ └───────────┘ └────┘ └┘ ┴
par └────┘ └──────┘ └───────────┘ └────┘ └┘ ┴
pid ┴ └──────┘ ┴ └┘ ┴
st └───────────────┘└─────────────┘└─────────────┘└┘
268
269 theorem of_think_terminates {s : computation α} :
id └─────────┘ ┴
src └─────────┘
typ └─────────┘ ┴
doc └─────────┘
270 terminates (think s) → terminates s
id └────────┘ └───┘ ┴ ┴ └────────┘ ┴
src └────────┘ └───┘ └────────┘
typ └────────┘ └───┘ ┴ ┴ └────────┘ ┴
doc └────────┘ └───┘ └────────┘
271 | ⟨a, h⟩ := ⟨a, of_think_mem h⟩
id ┴ ┴ └──────────┘
src └──────────┘
typ ┴ ┴ └──────────┘
272
273 theorem not_mem_empty (a : α) : a ∉ empty α :=
id ┴ ┴ ┴ └───┘ ┴
src ┴ └───┘
typ ┴ ┴ ┴ └───┘ ┴
doc └───┘
274 λ ⟨n, h⟩, by clear _fun_match; contradiction
id ┴
src └──────────────┘ └─────────────
typ ┴ └──────────────┘ └─────────────
doc └──────────────┘ └─────────────
txt └──────────────┘ └─────────────
par └──────────────┘ └─────────────
pid └─────────┘ └
st └────────────────────────────────
275
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
276 theorem not_terminates_empty : ¬ terminates (empty α) :=
id ┴ └────────┘ └───┘ ┴
src ┴ └────────┘ └───┘
typ ┴ └────────┘ └───┘ ┴
doc └────────┘ └───┘
277 λ ⟨a, h⟩, not_mem_empty a h
id ┴┴ ┴ └───────────┘
src └───────────┘
typ ┴┴ ┴ └───────────┘
278
279 theorem eq_empty_of_not_terminates {s} (H : ¬ terminates s) : s = empty α :=
id ┴ └────────┘ ┴ ┴ ┴ └───┘ ┴
src ┴ └────────┘ ┴ └───┘
typ ┴ └────────┘ ┴ ┴ ┴ └───┘ ┴
doc └────────┘ └───┘
280 begin
st └─────
281 apply subtype.eq, funext n,
id └────────┘
src └────┘└────────┘ └──────┘
typ └────┘└────────┘ └──────┘
doc └────┘ └──────┘
txt └────┘ └──────┘
par └────┘ └──────┘
pid ┴ └┘
st ─────────────────┘└────────┘└─
282 induction h : s.val n, {refl},
id └───┘ ┴
src └────────┘ └─┘└───┘┴ └──┘
typ └────────┘ └─┘└───┘┴┴ └──┘
doc └────────┘ └─┘ ┴ └──┘
txt └────────┘ └─┘ ┴ └──┘
par └────────┘ └─┘ ┴ └──┘
pid ┴ └─┘ ┴
st ──────────────────────┘└─────┘└┘└
283 refine absurd _ H, exact ⟨_, _, h.symm⟩
id └────┘ ┴ └────┘
src └─────┘└────┘└─┘ └────┘ └────┘└────┘└┘
typ └─────┘└────┘└─┘┴ └────┘ └────┘└────┘└┘
doc └─────┘ └─┘ └────┘ └────┘ └┘
txt └─────┘ └─┘ └────┘ └────┘ └┘
par └─────┘ └─┘ └────┘ └────┘ └┘
pid ┴ └─┘ ┴ └────┘ ┴┴
st ──────────────────┘└─────────────────────┘
284 end
st └─┘
285
286 theorem thinkN_mem {s : computation α} {a} : ∀ n, a ∈ thinkN s n ↔ a ∈ s
id └─────────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────┘ ┴ └────┘ ┴ ┴
typ └─────────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────────┘ └────┘
287 | 0 := iff.rfl
id └─────┘
src └─────┘
typ └─────┘
288 | (n+1) := iff.trans ⟨of_think_mem, think_mem⟩ (thinkN_mem n)
id ┴┴ └───────┘ └──────────┘ └───────┘ └────────┘
src ┴ └───────┘ └──────────┘ └───────┘
typ ┴┴ └───────┘ └──────────┘ └───────┘ └────────┘
289
290 instance thinkN_terminates (s : computation α) :
id └─────────┘ ┴
src └─────────┘
typ └─────────┘ ┴
doc └─────────┘
291 ∀ [terminates s] n, terminates (thinkN s n)
id ┴└────────┘ ┴ ┴ └────────┘ └────┘ ┴ ┴
src └────────┘ └────────┘ └────┘
typ ┴└────────┘ ┴ ┴ └────────┘ └────┘ ┴ ┴
doc └────────┘ └────────┘ └────┘
292 | ⟨a, h⟩ n := ⟨a, (thinkN_mem n).2 h⟩
id ┴ ┴ ┴ └────────┘ ┴
src └────────┘ ┴
typ ┴ ┴ ┴ └────────┘ ┴
293
294 theorem of_thinkN_terminates (s : computation α) (n) :
id └─────────┘ ┴
src └─────────┘
typ └─────────┘ ┴
doc └─────────┘
295 terminates (thinkN s n) → terminates s
id └────────┘ └────┘ ┴ ┴ ┴ └────────┘ ┴
src └────────┘ └────┘ └────────┘
typ └────────┘ └────┘ ┴ ┴ ┴ └────────┘ ┴
doc └────────┘ └────┘ └────────┘
296 | ⟨a, h⟩ := ⟨a, (thinkN_mem _).1 h⟩
id ┴ ┴ └────────┘ ┴
src └────────┘ ┴
typ ┴ ┴ └────────┘ ┴
297
298 /-- `promises s a`, or `s ~> a`, asserts that although the computation `s`
299 may not terminate, if it does, then the result is `a`. -/
300 def promises (s : computation α) (a : α) : Prop := ∀ ⦃a'⦄, a' ∈ s → a = a'
id └─────────┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └┘
src └─────────┘ ┴ ┴
typ └─────────┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └┘
doc └─────────┘
301
302 infix ` ~> `:50 := promises
id └──────┘
src └──────┘
typ └──────┘
doc └──────┘
303
304 theorem mem_promises {s : computation α} {a : α} : a ∈ s → s ~> a :=
id └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
src └─────────┘ ┴ └┘
typ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
doc └─────────┘ └┘
305 λ h a', mem_unique h
id ┴ └┘ └────────┘ ┴
src └────────┘
typ ┴ └┘ └────────┘ ┴
306
307 theorem empty_promises (a : α) : empty α ~> a :=
id ┴ └───┘ ┴ └┘ ┴
src └───┘ └┘
typ ┴ └───┘ ┴ └┘ ┴
doc └───┘ └┘
308 λ a' h, absurd h (not_mem_empty _)
id └┘ ┴ └────┘ ┴ └───────────┘
src └────┘ └───────────┘
typ └┘ ┴ └────┘ ┴ └───────────┘
309
310 section get
311 variables (s : computation α) [h : terminates s]
id └─────────┘ └────────┘
src └─────────┘ └────────┘
typ └─────────┘ └────────┘
doc └─────────┘ └────────┘
312 include s h
313
314 /-- `length s` gets the number of steps of a terminating computation -/
315 def length : ℕ := nat.find ((terminates_def _).1 h)
id ┴ └──────┘ └────────────┘ ┴ ┴
src ┴ └──────┘ └────────────┘ ┴
typ ┴ └──────┘ └────────────┘ ┴ ┴
316
317 /-- `get s` returns the result of a terminating computation -/
318 def get : α := option.get (nat.find_spec $ (terminates_def _).1 h)
id ┴ └────────┘ └───────────┘ └────────────┘ ┴ ┴
src └────────┘ └───────────┘ └────────────┘ ┴
typ ┴ └────────┘ └───────────┘ └────────────┘ ┴ ┴
319
320 theorem get_mem : get s ∈ s :=
id └─┘ ┴ ┴ ┴
src └─┘ ┴
typ └─┘ ┴ ┴ ┴
doc └─┘
321 exists.intro (length s) (option.eq_some_of_is_some _).symm
id └──────────┘ └────┘ ┴ └───────────────────────┘ └──┘
src └──────────┘ └────┘ └───────────────────────┘ └──┘
typ └──────────┘ └────┘ ┴ └───────────────────────┘ └──┘
doc └────┘
322
323 theorem get_eq_of_mem {a} : a ∈ s → get s = a :=
id ┴ ┴ ┴ └─┘ ┴ ┴ ┴
src ┴ └─┘ ┴
typ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
doc └─┘
324 mem_unique (get_mem _)
id └────────┘ └─────┘
src └────────┘ └─────┘
typ └────────┘ └─────┘
325
326 theorem mem_of_get_eq {a} : get s = a → a ∈ s :=
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘
327 by intro h; rw ←h; apply get_mem
id ┴ └─────┘
src └─────┘ └──┘ └────┘└─────┘└
typ └─────┘ └──┘┴ └────┘└─────┘└
doc └─────┘ └──┘ └────┘ └
txt └─────┘ └──┘ └────┘ └
par └─────┘ └──┘ └────┘ └
pid └┘ └┘ ┴ └
st └──────────────────────────────
328
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
329 @[simp] theorem get_think : get (think s) = get s :=
id └─┘ └───┘ ┴ ┴ └─┘ ┴
src └─┘ └───┘ ┴ └─┘
typ └─┘ └───┘ ┴ ┴ └─┘ ┴
doc └──┘ └─┘ └───┘ └─┘
330 get_eq_of_mem _ $ let ⟨n, h⟩ := get_mem s in ⟨n+1, h⟩
id └───────────┘ └─┘ ┴ ┴ └─────┘ ┴ ┴
src └───────────┘ └─────┘ ┴
typ └───────────┘ └─┘ ┴ ┴ └─────┘ ┴ ┴
331
332 @[simp] theorem get_thinkN (n) : get (thinkN s n) = get s :=
id └─┘ └────┘ ┴ ┴ ┴ └─┘ ┴
src └─┘ └────┘ ┴ └─┘
typ └─┘ └────┘ ┴ ┴ ┴ └─┘ ┴
doc └──┘ └─┘ └────┘ └─┘
333 get_eq_of_mem _ $ (thinkN_mem _).2 (get_mem _)
id └───────────┘ └────────┘ ┴ └─────┘
src └───────────┘ └────────┘ ┴ └─────┘
typ └───────────┘ └────────┘ ┴ └─────┘
334
335 theorem get_promises : s ~> get s := λ a, get_eq_of_mem _
id ┴ └┘ └─┘ ┴ ┴ └───────────┘
src └┘ └─┘ └───────────┘
typ ┴ └┘ └─┘ ┴ ┴ └───────────┘
doc └┘ └─┘
336
337 theorem mem_of_promises {a} (p : s ~> a) : a ∈ s :=
id ┴ └┘ ┴ ┴ ┴ ┴
src └┘ ┴
typ ┴ └┘ ┴ ┴ ┴ ┴
doc └┘
338 by unfreezeI; cases h with a' h; rw p h; exact h
id ┴ ┴ ┴ ┴
src └───────┘ └────┘ └────────┘ └─┘ ┴ └────┘ └
typ └───────┘ └────┘┴└────────┘ └─┘┴┴┴ └────┘┴└
doc └───────┘ └────┘ └────────┘ └─┘ ┴ └────┘ └
txt └───────┘ └────┘ └────────┘ └─┘ ┴ └────┘ └
par └───────┘ └────┘ └────────┘ └─┘ ┴ └────┘ └
pid ┴ └────────┘ ┴ ┴ ┴ └
st └────────────────────────────────┘┴└───────────
339
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
340 theorem get_eq_of_promises {a} : s ~> a → get s = a :=
id ┴ └┘ ┴ └─┘ ┴ ┴ ┴
src └┘ └─┘ ┴
typ ┴ └┘ ┴ └─┘ ┴ ┴ ┴
doc └┘ └─┘
341 get_eq_of_mem _ ∘ mem_of_promises _
id └───────────┘ ┴ └─────────────┘
src └───────────┘ ┴ └─────────────┘
typ └───────────┘ ┴ └─────────────┘
342
343 end get
344
345 /-- `results s a n` completely characterizes a terminating computation:
346 it asserts that `s` terminates after exactly `n` steps, with result `a`. -/
347 def results (s : computation α) (a : α) (n : ℕ) :=
id └─────────┘ ┴ ┴ ┴
src └─────────┘ ┴
typ └─────────┘ ┴ ┴ ┴
doc └─────────┘
348 ∃ (h : a ∈ s), @length _ s (terminates_of_mem h) = n
id ┴ ┴ ┴ ┴ ┴ └────┘ ┴ └───────────────┘ ┴ ┴ ┴
src ┴ ┴ ┴ └────┘ └───────────────┘ ┴
typ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ └───────────────┘ ┴ ┴ ┴
doc └────┘
349
350 theorem results_of_terminates (s : computation α) [T : terminates s] :
id └─────────┘ ┴ └────────┘ ┴
src └─────────┘ └────────┘
typ └─────────┘ ┴ └────────┘ ┴
doc └─────────┘ └────────┘
351 results s (get s) (length s) :=
id └─────┘ ┴ └─┘ ┴ └────┘ ┴
src └─────┘ └─┘ └────┘
typ └─────┘ ┴ └─┘ ┴ └────┘ ┴
doc └─────┘ └─┘ └────┘
352 ⟨get_mem _, rfl⟩
id └─────┘ └─┘
src └─────┘ └─┘
typ └─────┘ └─┘
353
354 theorem results_of_terminates' (s : computation α) [T : terminates s] {a} (h : a ∈ s) :
id └─────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴
src └─────────┘ └────────┘ ┴
typ └─────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴
doc └─────────┘ └────────┘
355 results s a (length s) :=
id └─────┘ ┴ ┴ └────┘ ┴
src └─────┘ └────┘
typ └─────┘ ┴ ┴ └────┘ ┴
doc └─────┘ └────┘
356 by rw ←get_eq_of_mem _ h; apply results_of_terminates
id └───────────┘ ┴ └───────────────────┘
src └──┘└───────────┘└─┘ └────┘└───────────────────┘└
typ └──┘└───────────┘└─┘┴ └────┘└───────────────────┘└
doc └──┘ └─┘ └────┘ └
txt └──┘ └─┘ └────┘ └
par └──┘ └─┘ └────┘ └
pid └┘ └─┘ ┴ └
st └───────────────────────────────────────────────────
357
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
358 theorem results.mem {s : computation α} {a n} : results s a n → a ∈ s
id └─────────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────┘ └─────┘ ┴
typ └─────────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────────┘ └─────┘
359 | ⟨m, _⟩ := m
id ┴
typ ┴
360
361 theorem results.terminates {s : computation α} {a n} (h : results s a n) : terminates s :=
id └─────────┘ ┴ └─────┘ ┴ ┴ ┴ └────────┘ ┴
src └─────────┘ └─────┘ └────────┘
typ └─────────┘ ┴ └─────┘ ┴ ┴ ┴ └────────┘ ┴
doc └─────────┘ └─────┘ └────────┘
362 terminates_of_mem h.mem
id └───────────────┘ ┴└──┘
src └───────────────┘ └──┘
typ └───────────────┘ ┴└──┘
363
364 theorem results.length {s : computation α} {a n} [T : terminates s] :
id └─────────┘ ┴ └────────┘ ┴
src └─────────┘ └────────┘
typ └─────────┘ ┴ └────────┘ ┴
doc └─────────┘ └────────┘
365 results s a n → length s = n
id └─────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
src └─────┘ └────┘ ┴
typ └─────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
doc └─────┘ └────┘
366 | ⟨_, h⟩ := h
id ┴
typ ┴
367
368 theorem results.val_unique {s : computation α} {a b m n}
id └─────────┘ ┴
src └─────────┘
typ └─────────┘ ┴
doc └─────────┘
369 (h1 : results s a m) (h2 : results s b n) : a = b :=
id └─────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ └─────┘ ┴
typ └─────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ └─────┘
370 mem_unique h1.mem h2.mem
id └────────┘ └┘└──┘ └┘└──┘
src └────────┘ └──┘ └──┘
typ └────────┘ └┘└──┘ └┘└──┘
371
372 theorem results.len_unique {s : computation α} {a b m n}
id └─────────┘ ┴
src └─────────┘
typ └─────────┘ ┴
doc └─────────┘
373 (h1 : results s a m) (h2 : results s b n) : m = n :=
id └─────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ └─────┘ ┴
typ └─────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ └─────┘
374 by haveI := h1.terminates; haveI := h2.terminates; rw [←h1.length, h2.length]
id └───────────┘ └───────────┘
src └───────┘└───────────┘ └───────┘└───────────┘ └───┘ └┘ └─
typ └───────┘└───────────┘ └───────┘└───────────┘ └───┘└───────┘└┘└───────┘└─
doc └───────┘ └───────┘ └───┘ └┘ └─
txt └───────┘ └───────┘ └───┘ └┘ └─
par └───────┘ └───────┘ └───┘ └┘ └─
pid ┴└─┘ ┴└─┘ └─┘ └┘ ┴└
st └───────────────────────────────────────────────────┘└────────┘└─────────┘┴└
375
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
376 theorem exists_results_of_mem {s : computation α} {a} (h : a ∈ s) : ∃ n, results s a n :=
id └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴┴ └─────┘ ┴ ┴ ┴
src └─────────┘ ┴ ┴ ┴ └─────┘
typ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴┴ └─────┘ ┴ ┴ ┴
doc └─────────┘ └─────┘
377 by haveI := terminates_of_mem h; exact ⟨_, results_of_terminates' s h⟩
id └───────────────┘ ┴ └────────────────────┘ ┴ ┴
src └───────┘└───────────────┘┴ └────┘ └─┘└────────────────────┘┴ ┴ └─
typ └───────┘└───────────────┘┴┴ └────┘ └─┘└────────────────────┘┴┴┴┴└─
doc └───────┘ ┴ └────┘ └─┘ ┴ ┴ └─
txt └───────┘ ┴ └────┘ └─┘ ┴ ┴ └─
par └───────┘ ┴ └────┘ └─┘ ┴ ┴ └─
pid ┴└─┘ ┴ ┴ └─┘ ┴ ┴ ┴└
st └────────────────────────────────────────────────────────────────────
378
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
379 @[simp] theorem get_ret (a : α) : get (return a) = a :=
id ┴ └─┘ └────┘ ┴ ┴ ┴
src └─┘ └────┘ ┴
typ ┴ └─┘ └────┘ ┴ ┴ ┴
doc └──┘ └─┘ └────┘
380 get_eq_of_mem _ ⟨0, rfl⟩
id └───────────┘ └─┘
src └───────────┘ └─┘
typ └───────────┘ └─┘
381
382 @[simp] theorem length_ret (a : α) : length (return a) = 0 :=
id ┴ └────┘ └────┘ ┴ ┴
src └────┘ └────┘ ┴
typ ┴ └────┘ └────┘ ┴ ┴
doc └──┘ └────┘ └────┘
383 let h := computation.ret_terminates a in
id ┴ └────────────────────────┘ ┴
src └────────────────────────┘
typ ┴ └────────────────────────┘ ┴
384 nat.eq_zero_of_le_zero $ nat.find_min' ((terminates_def (return a)).1 h) rfl
id └────────────────────┘ └───────────┘ └────────────┘ └────┘ ┴ ┴ ┴ └─┘
src └────────────────────┘ └───────────┘ └────────────┘ └────┘ ┴ └─┘
typ └────────────────────┘ └───────────┘ └────────────┘ └────┘ ┴ ┴ ┴ └─┘
doc └────┘
385
386 theorem results_ret (a : α) : results (return a) a 0 :=
id ┴ └─────┘ └────┘ ┴ ┴
src └─────┘ └────┘
typ ┴ └─────┘ └────┘ ┴ ┴
doc └─────┘ └────┘
387 ⟨_, length_ret _⟩
id └────────┘
src └────────┘
typ └────────┘
388
389 @[simp] theorem length_think (s : computation α) [h : terminates s] :
id └─────────┘ ┴ └────────┘ ┴
src └─────────┘ └────────┘
typ └─────────┘ ┴ └────────┘ ┴
doc └──┘ └─────────┘ └────────┘
390 length (think s) = length s + 1 :=
id └────┘ └───┘ ┴ ┴ └────┘ ┴ ┴
src └────┘ └───┘ ┴ └────┘ ┴
typ └────┘ └───┘ ┴ ┴ └────┘ ┴ ┴
doc └────┘ └───┘ └────┘
391 begin
st └─────
392 apply le_antisymm,
id └─────────┘
src └────┘└─────────┘
typ └────┘└─────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────┘└─
393 { exact nat.find_min' _ (nat.find_spec ((terminates_def _).1 h)) },
id └───────────┘ └───────────┘ └────────────┘ ┴
src └────┘└───────────┘└─┘ └───────────┘┴ └────────────┘└────┘ └─┘
typ └────┘└───────────┘└─┘ └───────────┘┴ └────────────┘└────┘┴└─┘
doc └────┘ └─┘ ┴ └────┘ └─┘
txt └────┘ └─┘ ┴ └────┘ └─┘
par └────┘ └─┘ ┴ └────┘ └─┘
pid ┴ └─┘ ┴ └────┘ └┘┴
st ───┘└─────────────────────────────────────────────────────────────┘└┘└
394 { have : (option.is_some ((think s).val (length (think s))) : Prop) :=
id └────────────┘ └────┘ └───┘ ┴
src └─────┘ └────────────┘┴ ┴ └────┘ └────┘┴ └───┘┴ └────┘ └────
typ └─────┘ └────────────┘┴ ┴ └────┘ └────┘┴ └───┘┴┴└────┘ └────
doc └─────┘ ┴ ┴ └────┘ └────┘┴ └───┘┴ └────┘ └────
txt └─────┘ ┴ ┴ └────┘ ┴ ┴ └────┘ └────
par └─────┘ ┴ ┴ └────┘ ┴ ┴ └────┘ └────
pid └───┘└┘ ┴ ┴ └────┘ ┴ ┴ └────┘ ┴└───
st ─────────────────────────────────────────────────────────────────────────
395 nat.find_spec ((terminates_def _).1 s.think_terminates),
id └───────────┘ └────────────┘ └────────────────┘
src ─────┘└───────────┘┴ └────────────┘└────┘└────────────────┘┴
typ ─────┘└───────────┘┴ └────────────┘└────┘└────────────────┘┴
doc ─────┘ ┴ └────┘ ┴
txt ─────┘ ┴ └────┘ ┴
par ─────┘ ┴ └────┘ ┴
pid ─────┘ ┴ └────┘ ┴
st ────────────────────────────────────────────────────────────┘└─
396 cases length (think s) with n,
id └────┘ └───┘ ┴
src └────┘└────┘┴ └───┘┴ └──────┘
typ └────┘└────┘┴ └───┘┴┴└──────┘
doc └────┘└────┘┴ └───┘┴ └──────┘
txt └────┘ ┴ ┴ └──────┘
par └────┘ ┴ ┴ └──────┘
pid ┴ ┴ ┴ ┴└─────┘
st ────────────────────────────────┘└─
397 { contradiction },
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid ┴
st ─────┘└────────────┘└┘└
398 { apply nat.succ_le_succ, apply nat.find_min', apply this } }
id └──────────────┘ └───────────┘
src └────┘└──────────────┘ └────┘└───────────┘ └────┘ ┴
typ └────┘└──────────────┘ └────┘└───────────┘ └────┘ ┴
doc └────┘ └────┘ └────┘ ┴
txt └────┘ └────┘ └────┘ ┴
par └────┘ └────┘ └────┘ ┴
pid ┴ ┴ ┴ ┴
st ───────────────────────────┘└───────────────────┘└───────────┘└───
399 end
st ──┘
400
401 theorem results_think {s : computation α} {a n}
id └─────────┘ ┴
src └─────────┘
typ └─────────┘ ┴
doc └─────────┘
402 (h : results s a n) : results (think s) a (n + 1) :=
id └─────┘ ┴ ┴ ┴ └─────┘ └───┘ ┴ ┴ ┴ ┴
src └─────┘ └─────┘ └───┘ ┴
typ └─────┘ ┴ ┴ ┴ └─────┘ └───┘ ┴ ┴ ┴ ┴
doc └─────┘ └─────┘ └───┘
403 by haveI := h.terminates; exact ⟨think_mem h.mem, by rw [length_think, h.length]⟩
id └──────────┘ └───────┘ └───┘ └──────────┘
src └───────┘└──────────┘ └────┘ └───────┘┴└───┘└┘ ┴└──┘└──────────┘└┘ ┴└─
typ └───────┘└──────────┘ └────┘ └───────┘┴└───┘└┘ ┴└──┘└──────────┘└┘└──────┘┴└─
doc └───────┘ └────┘ ┴ └┘ ┴└──┘ └┘ ┴└─
txt └───────┘ └────┘ ┴ └┘ ┴└──┘ └┘ ┴└─
par └───────┘ └────┘ ┴ └┘ ┴└──┘ └┘ ┴└─
pid ┴└─┘ ┴ ┴ └┘ └───┘ └┘ └┘└
st └────────────────────────────────────────────────┘└───────────────┘└────────┘┴└─
404
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
405 theorem of_results_think {s : computation α} {a n}
id └─────────┘ ┴
src └─────────┘
typ └─────────┘ ┴
doc └─────────┘
406 (h : results (think s) a n) : ∃ m, results s a m ∧ n = m + 1 :=
id └─────┘ └───┘ ┴ ┴ ┴ ┴ ┴┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ └───┘ ┴ ┴ └─────┘ ┴ ┴ ┴
typ └─────┘ └───┘ ┴ ┴ ┴ ┴ ┴┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ └───┘ └─────┘
407 begin
st └─────
408 haveI := of_think_terminates h.terminates,
id └─────────────────┘ └──────────┘
src └───────┘└─────────────────┘┴└──────────┘
typ └───────┘└─────────────────┘┴└──────────┘
doc └───────┘ ┴
txt └───────┘ ┴
par └───────┘ ┴
pid ┴└─┘ ┴
st ──────────────────────────────────────────┘└─
409 have := results_of_terminates' _ (of_think_mem h.mem),
id └────────────────────┘ └──────────┘ └───┘
src └──────┘└────────────────────┘└─┘ └──────────┘┴└───┘┴
typ └──────┘└────────────────────┘└─┘ └──────────┘┴└───┘┴
doc └──────┘ └─┘ ┴ ┴
txt └──────┘ └─┘ ┴ ┴
par └──────┘ └─┘ ┴ ┴
pid └───┘└─┘ └─┘ ┴ ┴
st ──────────────────────────────────────────────────────┘└─
410 exact ⟨_, this, results.len_unique h (results_think this)⟩,
id └────────────────┘ ┴ └───────────┘ └──┘
src └────┘ └─┘ └┘└────────────────┘┴ ┴ └───────────┘┴ └┘
typ └────┘ └─┘ └┘└────────────────┘┴┴┴ └───────────┘┴└──┘└┘
doc └────┘ └─┘ └┘ ┴ ┴ ┴ └┘
txt └────┘ └─┘ └┘ ┴ ┴ ┴ └┘
par └────┘ └─┘ └┘ ┴ ┴ ┴ └┘
pid ┴ └─┘ └┘ ┴ ┴ ┴ └┘
st ───────────────────────────────────────────────────────────┘└─
411 end
st ──┘
412
413 @[simp] theorem results_think_iff {s : computation α} {a n} :
id └─────────┘ ┴
src └─────────┘
typ └─────────┘ ┴
doc └──┘ └─────────┘
414 results (think s) a (n + 1) ↔ results s a n :=
id └─────┘ └───┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴
src └─────┘ └───┘ ┴ ┴ └─────┘
typ └─────┘ └───┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴
doc └─────┘ └───┘ └─────┘
415 ⟨λ h, let ⟨n', r, e⟩ := of_results_think h in by injection e with h'; rwa h',
id ┴ └─┘ └──────────────┘ ┴ ┴ └┘
src └──────────────┘ └────────┘ └──────┘ └──┘
typ ┴ └─┘ └──────────────┘ ┴ └────────┘┴└──────┘ └──┘└┘
doc └────────┘ └──────┘ └──┘
txt └────────┘ └──────┘ └──┘
par └────────┘ └──────┘ └──┘
pid ┴ └──────┘ ┴
st └────────────────────────┘└┘
416 results_think⟩
id └───────────┘
src └───────────┘
typ └───────────┘
417
418 theorem results_thinkN {s : computation α} {a m} :
id └─────────┘ ┴
src └─────────┘
typ └─────────┘ ┴
doc └─────────┘
419 ∀ n, results s a m → results (thinkN s n) a (m + n)
id ┴ └─────┘ ┴ ┴ ┴ └─────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ └─────┘ └────┘ ┴
typ ┴ └─────┘ ┴ ┴ ┴ └─────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ └─────┘ └────┘
420 | 0 h := h
id ┴
typ ┴
421 | (n+1) h := results_think (results_thinkN n h)
id ┴┴ ┴ └───────────┘ └────────────┘
src ┴ └───────────┘
typ ┴┴ ┴ └───────────┘ └────────────┘
422
423 theorem results_thinkN_ret (a : α) (n) : results (thinkN (return a) n) a n :=
id ┴ └─────┘ └────┘ └────┘ ┴ ┴ ┴ ┴
src └─────┘ └────┘ └────┘
typ ┴ └─────┘ └────┘ └────┘ ┴ ┴ ┴ ┴
doc └─────┘ └────┘ └────┘
424 by have := results_thinkN n (results_ret a); rwa zero_add at this
id └────────────┘ ┴ └─────────┘ ┴ └──────┘
src └──────┘└────────────┘┴ ┴ └─────────┘┴ ┴ └──┘└──────┘└────────
typ └──────┘└────────────┘┴┴┴ └─────────┘┴┴┴ └──┘└──────┘└────────
doc └──────┘ ┴ ┴ ┴ ┴ └──┘ └────────
txt └──────┘ ┴ ┴ ┴ ┴ └──┘ └────────
par └──────┘ ┴ ┴ ┴ ┴ └──┘ └────────
pid └───┘└─┘ ┴ ┴ ┴ ┴ ┴ └──────┘└
st └─────────────────────────────────────────────┘└──────┘└────────
425
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
426 @[simp] theorem length_thinkN (s : computation α) [h : terminates s] (n) :
id └─────────┘ ┴ └────────┘ ┴
src └─────────┘ └────────┘
typ └─────────┘ ┴ └────────┘ ┴
doc └──┘ └─────────┘ └────────┘
427 length (thinkN s n) = length s + n :=
id └────┘ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
src └────┘ └────┘ ┴ └────┘ ┴
typ └────┘ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
doc └────┘ └────┘ └────┘
428 (results_thinkN n (results_of_terminates _)).length
id └────────────┘ ┴ └───────────────────┘ └────┘
src └────────────┘ └───────────────────┘ └────┘
typ └────────────┘ ┴ └───────────────────┘ └────┘
429
430 theorem eq_thinkN {s : computation α} {a n} (h : results s a n) :
id └─────────┘ ┴ └─────┘ ┴ ┴ ┴
src └─────────┘ └─────┘
typ └─────────┘ ┴ └─────┘ ┴ ┴ ┴
doc └─────────┘ └─────┘
431 s = thinkN (return a) n :=
id ┴ ┴ └────┘ └────┘ ┴ ┴
src ┴ └────┘ └────┘
typ ┴ ┴ └────┘ └────┘ ┴ ┴
doc └────┘ └────┘
432 begin
st └─────
433 revert s,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └┘
st ─────────┘└─
434 induction n with n IH; intro s;
id ┴
src └────────┘ └────────┘ └─────┘
typ └────────┘┴└────────┘ └─────┘
doc └────────┘ └────────┘ └─────┘
txt └────────┘ └────────┘ └─────┘
par └────────┘ └────────┘ └─────┘
pid ┴ ┴└───────┘ └┘
st ──────────────────────────────────
435 apply cases_on s (λ a', _) (λ s, _); intro h,
id └──────┘ ┴
src └────┘└──────┘┴ ┴ └──────┘ └────┘ └─────┘
typ └────┘└──────┘┴┴┴ └──────┘ └────┘ └─────┘
doc └────┘ ┴ ┴ └──────┘ └────┘ └─────┘
txt └────┘ ┴ ┴ └──────┘ └────┘ └─────┘
par └────┘ ┴ ┴ └──────┘ └────┘ └─────┘
pid ┴ ┴ ┴ └──────┘ └────┘ └┘
st ─────────────────────────────────────────────┘└─
436 { rw ←eq_of_ret_mem h.mem, refl },
id └───────────┘ └───┘
src └──┘└───────────┘┴└───┘ └───┘
typ └──┘└───────────┘┴└───┘ └───┘
doc └──┘ ┴ └───┘
txt └──┘ ┴ └───┘
par └──┘ ┴ └───┘
pid └┘ ┴ ┴
st ───┘└─────────────────────┘└─────┘└┘└
437 { cases of_results_think h with n h, cases h, contradiction },
id └──────────────┘ ┴ ┴
src └────┘└──────────────┘┴ └───────┘ └────┘ └────────────┘
typ └────┘└──────────────┘┴┴└───────┘ └────┘┴ └────────────┘
doc └────┘ ┴ └───────┘ └────┘ └────────────┘
txt └────┘ ┴ └───────┘ └────┘ └────────────┘
par └────┘ ┴ └───────┘ └────┘ └────────────┘
pid ┴ ┴ └───────┘ ┴ ┴
st ───┘└───────────────────────────────┘└───────┘└──────────────┘└┘└
438 { have := h.len_unique (results_ret _), contradiction },
id └──────────┘ └─────────┘
src └──────┘└──────────┘┴ └─────────┘└─┘ └────────────┘
typ └──────┘└──────────┘┴ └─────────┘└─┘ └────────────┘
doc └──────┘ ┴ └─┘ └────────────┘
txt └──────┘ ┴ └─┘ └────────────┘
par └──────┘ ┴ └─┘ └────────────┘
pid └───┘└─┘ ┴ └─┘ ┴
st ───┘└──────────────────────────────────┘└──────────────┘└┘└
439 { rw IH (results_think_iff.1 h), refl }
id └┘ └───────────────┘ ┴
src └─┘ ┴ └───────────────┘└─┘ ┴ └───┘
typ └─┘└┘┴ └───────────────┘└─┘┴┴ └───┘
doc └─┘ ┴ └─┘ ┴ └───┘
txt └─┘ ┴ └─┘ ┴ └───┘
par └─┘ ┴ └─┘ ┴ └───┘
pid ┴ ┴ └─┘ ┴ ┴
st ────────────────────────────────┘└─────┘└─
440 end
st ──┘
441
442 theorem eq_thinkN' (s : computation α) [h : terminates s] :
id └─────────┘ ┴ └────────┘ ┴
src └─────────┘ └────────┘
typ └─────────┘ ┴ └────────┘ ┴
doc └─────────┘ └────────┘
443 s = thinkN (return (get s)) (length s) :=
id ┴ ┴ └────┘ └────┘ └─┘ ┴ └────┘ ┴
src ┴ └────┘ └────┘ └─┘ └────┘
typ ┴ ┴ └────┘ └────┘ └─┘ ┴ └────┘ ┴
doc └────┘ └────┘ └─┘ └────┘
444 eq_thinkN (results_of_terminates _)
id └───────┘ └───────────────────┘
src └───────┘ └───────────────────┘
typ └───────┘ └───────────────────┘
445
446 def mem_rec_on {C : computation α → Sort v} {a s} (M : a ∈ s)
id └─────────┘ ┴ ┴ ┴ ┴
src └─────────┘ ┴
typ └─────────┘ ┴ ┴ ┴ ┴
doc └─────────┘
447 (h1 : C (return a)) (h2 : ∀ s, C s → C (think s)) : C s :=
id ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
src └────┘ └───┘
typ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
doc └────┘ └───┘
448 begin
st └─────
449 haveI T := terminates_of_mem M,
id └───────────────┘ ┴
src └─────────┘└───────────────┘┴
typ └─────────┘└───────────────┘┴┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid └┘┴└─┘ ┴
st ───────────────────────────────┘└─
450 rw [eq_thinkN' s, get_eq_of_mem s M],
id └────────┘ ┴ └───────────┘ ┴ ┴
src └──┘└────────┘┴ └┘└───────────┘┴ ┴ ┴
typ └──┘└────────┘┴┴└┘└───────────┘┴┴┴┴┴
doc └──┘ ┴ └┘ ┴ ┴ ┴
txt └──┘ ┴ └┘ ┴ ┴ ┴
par └──┘ ┴ └┘ ┴ ┴ ┴
pid └┘ ┴ └┘ ┴ ┴ ┴
st ─────────────────┘└─────────────────┘└──
451 generalize : length s = n,
id └────┘ ┴
src └───────────┘└────┘┴ ┴ ┴
typ └───────────┘└────┘┴┴┴ ┴
doc └───────────┘└────┘┴ ┴ ┴
txt └───────────┘ ┴ ┴ ┴
par └───────────┘ ┴ ┴ ┴
pid ┴┴┴ ┴ ┴ ┴
st ──────────────────────────┘└─
452 induction n with n IH, exacts [h1, h2 _ IH]
id ┴ └┘ └┘ └┘
src └────────┘ └────────┘ └──────┘ └┘ └─┘ └┘
typ └────────┘┴└────────┘ └──────┘└┘└┘└┘└─┘└┘└┘
doc └────────┘ └────────┘ └──────┘ └┘ └─┘ └┘
txt └────────┘ └────────┘ └──────┘ └┘ └─┘ └┘
par └────────┘ └────────┘ └──────┘ └┘ └─┘ └┘
pid ┴ ┴└───────┘ └┘ └┘ └─┘ ┴┴
st ──────────────────────┘└─────────────────────┘
453 end
st └─┘
454
455 def terminates_rec_on {C : computation α → Sort v} (s) [terminates s]
id └─────────┘ ┴ └────────┘ ┴
src └─────────┘ └────────┘
typ └─────────┘ ┴ └────────┘ ┴
doc └─────────┘ └────────┘
456 (h1 : ∀ a, C (return a)) (h2 : ∀ s, C s → C (think s)) : C s :=
id ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
src └────┘ └───┘
typ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
doc └────┘ └───┘
457 mem_rec_on (get_mem s) (h1 _) h2
id └────────┘ └─────┘ ┴ └┘ └┘
src └────────┘ └─────┘
typ └────────┘ └─────┘ ┴ └┘ └┘
458
459 /-- Map a function on the result of a computation. -/
460 def map (f : α → β) : computation α → computation β
id ┴ ┴ └─────────┘ ┴ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ ┴ ┴ └─────────┘ ┴ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
461 | ⟨s, al⟩ := ⟨s.map (λo, option.cases_on o none (some ∘ f)),
id ┴ └──┘ ┴ └─────────────┘ ┴ └──┘ └──┘ ┴ ┴
src └──┘ └─────────────┘ └──┘ └──┘ ┴
typ ┴ └──┘ ┴ └─────────────┘ ┴ └──┘ └──┘ ┴ ┴
462 λn b, begin
id ┴ ┴
typ ┴ ┴
st └─────
463 dsimp [stream.map, stream.nth],
id └────────┘ └────────┘
src └─────┘└────────┘└┘└────────┘┴
typ └─────┘└────────┘└┘└────────┘┴
doc └─────┘ └┘ ┴
txt └─────┘ └┘ ┴
par └─────┘ └┘ ┴
pid ┴┴ └┘ ┴
st ───────────────────────────────┘└─
464 induction e : s n with a; intro h,
id ┴ ┴
src └────────┘ └─┘ ┴ └─────┘ └─────┘
typ └────────┘ └─┘┴┴┴└─────┘ └─────┘
doc └────────┘ └─┘ ┴ └─────┘ └─────┘
txt └────────┘ └─┘ ┴ └─────┘ └─────┘
par └────────┘ └─┘ ┴ └─────┘ └─────┘
pid ┴ └─┘ ┴ ┴└────┘ └┘
st ──────────────────────────────────┘└─
465 { contradiction }, { rw [al e, ←h] }
id └┘ ┴ ┴
src └────────────┘ └──┘ ┴ └─┘ └┘
typ └────────────┘ └──┘└┘┴┴└─┘┴└┘
doc └────────────┘ └──┘ ┴ └─┘ └┘
txt └────────────┘ └──┘ ┴ └─┘ └┘
par └────────────┘ └──┘ ┴ └─┘ └┘
pid ┴ └┘ ┴ └─┘ ┴┴
st ───┘└────────────┘└┘└─────────┘└──┘┴┴└─
466 end⟩
st ──┘
467
468 def bind.G : β ⊕ computation β → β ⊕ computation α ⊕ computation β
id ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ └─────────┘ ┴ ┴ └─────────┘ ┴
src ┴ └─────────┘ ┴ └─────────┘ ┴ └─────────┘
typ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ └─────────┘ ┴ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘ └─────────┘
469 | (sum.inl b) := sum.inl b
id └─────┘ ┴ └─────┘
src └─────┘ └─────┘
typ └─────┘ ┴ └─────┘
470 | (sum.inr cb') := sum.inr $ sum.inr cb'
id └─────┘ └─┘ └─────┘ └─────┘
src └─────┘ └─────┘ └─────┘
typ └─────┘ └─┘ └─────┘ └─────┘
471
472 def bind.F (f : α → computation β) :
id ┴ └─────────┘ ┴
src └─────────┘
typ ┴ └─────────┘ ┴
doc └─────────┘
473 computation α ⊕ computation β → β ⊕ computation α ⊕ computation β
id └─────────┘ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ └─────────┘ ┴ ┴ └─────────┘ ┴
src └─────────┘ ┴ └─────────┘ ┴ └─────────┘ ┴ └─────────┘
typ └─────────┘ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ └─────────┘ ┴ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘ └─────────┘ └─────────┘
474 | (sum.inl ca) :=
id └─────┘ └┘
src └─────┘
typ └─────┘ └┘
475 match destruct ca with
id └──────┘
src └──────┘
typ └──────┘
doc └──────┘
476 | sum.inl a := bind.G $ destruct (f a)
id └─────┘ ┴ └────┘ └──────┘ ┴
src └─────┘ └────┘ └──────┘
typ └─────┘ ┴ └────┘ └──────┘ ┴
doc └──────┘
477 | sum.inr ca' := sum.inr $ sum.inl ca'
id └─────┘ └─┘ └─────┘ └─────┘
src └─────┘ └─────┘ └─────┘
typ └─────┘ └─┘ └─────┘ └─────┘
478 end
479 | (sum.inr cb) := bind.G $ destruct cb
id └─────┘ └┘ └────┘ └──────┘
src └─────┘ └────┘ └──────┘
typ └─────┘ └┘ └────┘ └──────┘
doc └──────┘
480
481 /-- Compose two computations into a monadic `bind` operation. -/
482 def bind (c : computation α) (f : α → computation β) : computation β :=
id └─────────┘ ┴ ┴ └─────────┘ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘ └─────────┘
typ └─────────┘ ┴ ┴ └─────────┘ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘ └─────────┘
483 corec (bind.F f) (sum.inl c)
id └───┘ └────┘ ┴ └─────┘ ┴
src └───┘ └────┘ └─────┘
typ └───┘ └────┘ ┴ └─────┘ ┴
doc └───┘
484
485 instance : has_bind computation := ⟨@bind⟩
id └──────┘ └─────────┘ └──┘
src └──────┘ └─────────┘ └──┘
typ └──────┘ └─────────┘ └──┘
doc └─────────┘ └──┘
486
487 theorem has_bind_eq_bind {β} (c : computation α) (f : α → computation β) :
id └─────────┘ ┴ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ └─────────┘ ┴ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
488 c >>= f = bind c f := rfl
id ┴ └─┘ ┴ ┴ └──┘ ┴ ┴ └─┘
src └─┘ ┴ └──┘ └─┘
typ ┴ └─┘ ┴ ┴ └──┘ ┴ ┴ └─┘
doc └──┘
489
490 /-- Flatten a computation of computations into a single computation. -/
491 def join (c : computation (computation α)) : computation α := c >>= id
id └─────────┘ └─────────┘ ┴ └─────────┘ ┴ ┴ └─┘ └┘
src └─────────┘ └─────────┘ └─────────┘ └─┘ └┘
typ └─────────┘ └─────────┘ ┴ └─────────┘ ┴ ┴ └─┘ └┘
doc └─────────┘ └─────────┘ └─────────┘
492
493 @[simp] theorem map_ret (f : α → β) (a) : map f (return a) = return (f a) := rfl
id ┴ ┴ └─┘ ┴ └────┘ ┴ ┴ └────┘ ┴ ┴ └─┘
src └─┘ └────┘ ┴ └────┘ └─┘
typ ┴ ┴ └─┘ ┴ └────┘ ┴ ┴ └────┘ ┴ ┴ └─┘
doc └──┘ └─┘ └────┘ └────┘
494
495 @[simp] theorem map_think (f : α → β) : ∀ s, map f (think s) = think (map f s)
id ┴ ┴ ┴ └─┘ ┴ └───┘ ┴ ┴ └───┘ └─┘ ┴ ┴
src └─┘ └───┘ ┴ └───┘ └─┘
typ ┴ ┴ ┴ └─┘ ┴ └───┘ ┴ ┴ └───┘ └─┘ ┴ ┴
doc └──┘ └─┘ └───┘ └───┘ └─┘
496 | ⟨s, al⟩ := by apply subtype.eq; dsimp [think, map]; rw stream.map_cons
id └────────┘ └───┘ └─┘ └─────────────┘
src └────┘└────────┘ └─────┘└───┘└┘└─┘┴ └─┘└─────────────┘└
typ └────┘└────────┘ └─────┘└───┘└┘└─┘┴ └─┘└─────────────┘└
doc └────┘ └─────┘└───┘└┘└─┘┴ └─┘ └
txt └────┘ └─────┘ └┘ ┴ └─┘ └
par └────┘ └─────┘ └┘ ┴ └─┘ └
pid ┴ ┴┴ └┘ ┴ ┴ └
st └────────────────────────────────────────┘└─────────────┘└
497
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
498 @[simp] theorem destruct_map (f : α → β) (s) : destruct (map f s) = lmap f (rmap (map f) (destruct s)) :=
id ┴ ┴ └──────┘ └─┘ ┴ ┴ ┴ └──┘ ┴ └──┘ └─┘ ┴ └──────┘ ┴
src └──────┘ └─┘ ┴ └──┘ └──┘ └─┘ └──────┘
typ ┴ ┴ └──────┘ └─┘ ┴ ┴ ┴ └──┘ ┴ └──┘ └─┘ ┴ └──────┘ ┴
doc └──┘ └──────┘ └─┘ └──┘ └──┘ └─┘ └──────┘
499 by apply s.cases_on; intro; simp
src └────┘ └───┘ └────
typ └────┘ └───┘ └────
doc └────┘ └───┘ └────
txt └────┘ └───┘ └────
par └────┘ └───┘ └────
pid ┴ └
st └──────────────────────────────
500
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
501 @[simp] theorem map_id : ∀ (s : computation α), map id s = s
id ┴ └─────────┘ ┴ └─┘ └┘ ┴ ┴ ┴
src └─────────┘ └─┘ └┘ ┴
typ ┴ └─────────┘ ┴ └─┘ └┘ ┴ ┴ ┴
doc └──┘ └─────────┘ └─┘
502 | ⟨f, al⟩ := begin
st └─────
503 apply subtype.eq; simp [map, function.comp],
id └────────┘ └─┘ └───────────┘
src └────┘└────────┘ └────┘└─┘└┘└───────────┘┴
typ └────┘└────────┘ └────┘└─┘└┘└───────────┘┴
doc └────┘ └────┘└─┘└┘ ┴
txt └────┘ └────┘ └┘ ┴
par └────┘ └────┘ └┘ ┴
pid ┴ ┴┴ └┘ ┴
st ────────────────────────────────────────────┘└─
504 have e : (@option.rec α (λ_, option α) none some) = id,
id └────────┘ └────┘ ┴ └──┘ └──┘ ┴ └┘
src └───────┘ └────────┘┴ ┴ └─┘└────┘┴ └┘└──┘┴└──┘└┘┴┴└┘
typ └───────┘ └────────┘┴ ┴ └─┘└────┘┴┴└┘└──┘┴└──┘└┘┴┴└┘
doc └───────┘ ┴ ┴ └─┘ ┴ └┘ ┴ └┘ ┴
txt └───────┘ ┴ ┴ └─┘ ┴ └┘ ┴ └┘ ┴
par └───────┘ ┴ ┴ └─┘ ┴ └┘ ┴ └┘ ┴
pid └────┘└─┘ ┴ ┴ └─┘ ┴ └┘ ┴ └┘ ┴
st ───────────────────────────────────────────────────────┘└─
505 { funext x, cases x; refl },
id ┴
src └──────┘ └────┘ └───┘
typ └──────┘ └────┘┴ └───┘
doc └──────┘ └────┘ └───┘
txt └──────┘ └────┘ └───┘
par └──────┘ └────┘ └───┘
pid └┘ ┴ ┴
st ───┘└──────┘└──────────────┘└┘└
506 simp [e, stream.map_id]
id ┴ └───────────┘
src └────┘ └┘└───────────┘└┘
typ └────┘┴└┘└───────────┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st ─────────────────────────┘
507 end
st └─┘
508
509 theorem map_comp (f : α → β) (g : β → γ) :
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
510 ∀ (s : computation α), map (g ∘ f) s = map g (map f s)
id ┴ └─────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴
src └─────────┘ └─┘ ┴ ┴ └─┘ └─┘
typ ┴ └─────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴
doc └─────────┘ └─┘ └─┘ └─┘
511 | ⟨s, al⟩ := begin
st └─────
512 apply subtype.eq; dsimp [map],
id └────────┘ └─┘
src └────┘└────────┘ └─────┘└─┘┴
typ └────┘└────────┘ └─────┘└─┘┴
doc └────┘ └─────┘└─┘┴
txt └────┘ └─────┘ ┴
par └────┘ └─────┘ ┴
pid ┴ ┴┴ ┴
st ──────────────────────────────┘└─
513 rw stream.map_map,
id └────────────┘
src └─┘└────────────┘
typ └─┘└────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────────────────┘└─
514 apply congr_arg (λ f : _ → option γ, stream.map f s),
id └───────┘ ┴ └────┘ ┴ └────────┘ ┴
src └────┘└───────┘┴ └─────┘ ┴└────┘┴ └┘└────────┘┴ ┴ ┴
typ └────┘└───────┘┴ └─────┘┴┴└────┘┴┴└┘└────────┘┴ ┴┴┴
doc └────┘ ┴ └─────┘ ┴ ┴ └┘ ┴ ┴ ┴
txt └────┘ ┴ └─────┘ ┴ ┴ └┘ ┴ ┴ ┴
par └────┘ ┴ └─────┘ ┴ ┴ └┘ ┴ ┴ ┴
pid ┴ ┴ └─────┘ ┴ ┴ └┘ ┴ ┴ ┴
st ─────────────────────────────────────────────────────┘└─
515 funext x, cases x with x; refl
id ┴
src └──────┘ └────┘ └─────┘ └───┘
typ └──────┘ └────┘┴└─────┘ └───┘
doc └──────┘ └────┘ └─────┘ └───┘
txt └──────┘ └────┘ └─────┘ └───┘
par └──────┘ └────┘ └─────┘ └───┘
pid └┘ ┴ └─────┘ ┴
st ─────────┘└─────────────────────┘
516 end
st └─┘
517
518 @[simp] theorem ret_bind (a) (f : α → computation β) :
id ┴ └─────────┘ ┴
src └─────────┘
typ ┴ └─────────┘ ┴
doc └──┘ └─────────┘
519 bind (return a) f = f a :=
id └──┘ └────┘ ┴ ┴ ┴ ┴ ┴
src └──┘ └────┘ ┴
typ └──┘ └────┘ ┴ ┴ ┴ ┴ ┴
doc └──┘ └────┘
520 begin
st └─────
521 apply eq_of_bisim (λc₁ c₂,
id └─────────┘
src └────┘└─────────┘┴ └──────
typ └────┘└─────────┘┴ └──────
doc └────┘ ┴ └──────
txt └────┘ ┴ └──────
par └────┘ ┴ └──────
pid ┴ ┴ └──────
st ─────────────────────────────
522 c₁ = bind (return a) f ∧ c₂ = f a ∨
id ┴ └──┘ └────┘ ┴ ┴ ┴
src ────────┘ ┴┴┴└──┘┴ └────┘┴ └┘ ┴┴┴ ┴ ┴ ┴ ┴┴└
typ ────────┘ ┴┴┴└──┘┴ └────┘┴ └┘ ┴┴┴ ┴ ┴ ┴┴┴┴└
doc ────────┘ ┴ ┴└──┘┴ └────┘┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └
txt ────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └
par ────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └
pid ────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └
st ─────────────────────────────────────────────
523 c₁ = corec (bind.F f) (sum.inr c₂)),
id └───┘ └────┘ ┴ └─────┘
src ────────┘ ┴ ┴└───┘┴ └────┘┴ └┘ └─────┘┴ └┘
typ ────────┘ ┴ ┴└───┘┴ └────┘┴┴└┘ └─────┘┴ └┘
doc ────────┘ ┴ ┴└───┘┴ ┴ └┘ ┴ └┘
txt ────────┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘
par ────────┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘
pid ────────┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘
st ───────────────────────────────────────────┘└─
524 { intros c₁ c₂ h,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └──────┘
st ───┘└────────────┘└─
525 exact match c₁, c₂, h with
id └┘ └┘ ┴
src └────┘ ┴ └┘ └┘ └─────
typ └────┘ ┴└┘└┘└┘└┘┴└─────
doc └────┘ ┴ └┘ └┘ └─────
txt └────┘ ┴ └┘ └┘ └─────
par └────┘ ┴ └┘ └┘ └─────
pid ┴ ┴ └┘ └┘ └─────
st ───────────────────────────────
526 | ._, ._, or.inl ⟨rfl, rfl⟩ := begin
id └────┘ └─┘
src ─────┘ └┘ └┘└────┘┴ └┘└─┘└───┘ └
typ ─────┘ └┘ └┘└────┘┴ └┘└─┘└───┘ └
doc ─────┘ └┘ └┘ ┴ └┘ └───┘ └
txt ─────┘ └┘ └┘ ┴ └┘ └───┘ └
par ─────┘ └┘ └┘ ┴ └┘ └───┘ └
pid ─────┘ └┘ └┘ ┴ └┘ └───┘ └
st ──────────────────────────────────┘└─────
527 simp [bind, bind.F],
id └──┘ └────┘
src ─────┘└────┘└──┘└┘└────┘┴└─
typ ─────┘└────┘└──┘└┘└────┘┴└─
doc ─────┘└────┘└──┘└┘ ┴└─
txt ─────┘└────┘ └┘ ┴└─
par ─────┘└────┘ └┘ ┴└─
pid ───────────┘ └┘ └──
st ────────────────────────┘└─
528 cases destruct (f a) with b cb; simp [bind.G]
id └──────┘ ┴ ┴ └────┘
src ─────┘└────┘└──────┘┴ ┴ └─────────┘└┘└────┘└────┘└─
typ ─────┘└────┘└──────┘┴ ┴┴┴└─────────┘└┘└────┘└────┘└─
doc ─────┘└────┘└──────┘┴ ┴ └─────────┘└┘└────┘ └─
txt ─────┘└────┘ ┴ ┴ └─────────┘└┘└────┘ └─
par ─────┘└────┘ ┴ ┴ └─────────┘└┘└────┘ └─
pid ───────────┘ ┴ ┴ └─────────────────┘ └─
st ────────────────────────────────────────────────────
529 end
src ───┘└───
typ ───┘└───
doc ───┘└───
txt ───┘└───
par ───┘└───
pid ────────
st ───┘└─┘└
530 | ._, c, or.inr rfl := begin
id └────┘
src ─────┘ └┘ └┘└────┘┴ └──┘ └
typ ─────┘ └┘ └┘└────┘┴ └──┘ └
doc ─────┘ └┘ └┘ ┴ └──┘ └
txt ─────┘ └┘ └┘ ┴ └──┘ └
par ─────┘ └┘ └┘ ┴ └──┘ └
pid ─────┘ └┘ └┘ ┴ └──┘ └
st ──────────────────────────┘└─────
531 simp [bind.F],
id └────┘
src ─────┘└────┘└────┘┴└─
typ ─────┘└────┘└────┘┴└─
doc ─────┘└────┘ ┴└─
txt ─────┘└────┘ ┴└─
par ─────┘└────┘ ┴└─
pid ───────────┘ └──
st ──────────────────┘└─
532 cases destruct c with b cb; simp [bind.G]
id └──────┘ ┴ └────┘
src ─────┘└────┘└──────┘┴ └────────┘└┘└────┘└────┘└─
typ ─────┘└────┘└──────┘┴┴└────────┘└┘└────┘└────┘└─
doc ─────┘└────┘└──────┘┴ └────────┘└┘└────┘ └─
txt ─────┘└────┘ ┴ └────────┘└┘└────┘ └─
par ─────┘└────┘ ┴ └────────┘└┘└────┘ └─
pid ───────────┘ ┴ └────────────────┘ └─
st ────────────────────────────────────────────────
533 end end },
src ───┘└──────┘
typ ───┘└──────┘
doc ───┘└──────┘
txt ───┘└──────┘
par ───┘└──────┘
pid ──────────┘┴
st ───┘└─┘└───┘└┘└
534 { simp }
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ────────┘└─
535 end
st ──┘
536
537 @[simp] theorem think_bind (c) (f : α → computation β) :
id ┴ └─────────┘ ┴
src └─────────┘
typ ┴ └─────────┘ ┴
doc └──┘ └─────────┘
538 bind (think c) f = think (bind c f) :=
id └──┘ └───┘ ┴ ┴ ┴ └───┘ └──┘ ┴ ┴
src └──┘ └───┘ ┴ └───┘ └──┘
typ └──┘ └───┘ ┴ ┴ ┴ └───┘ └──┘ ┴ ┴
doc └──┘ └───┘ └───┘ └──┘
539 destruct_eq_think $ by simp [bind, bind.F]
id └───────────────┘ └──┘ └────┘
src └───────────────┘ └────┘└──┘└┘└────┘└─
typ └───────────────┘ └────┘└──┘└┘└────┘└─
doc └────┘└──┘└┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └────────────────────
540
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
541 @[simp] theorem bind_ret (f : α → β) (s) : bind s (return ∘ f) = map f s :=
id ┴ ┴ └──┘ ┴ └────┘ ┴ ┴ ┴ └─┘ ┴ ┴
src └──┘ └────┘ ┴ ┴ └─┘
typ ┴ ┴ └──┘ ┴ └────┘ ┴ ┴ ┴ └─┘ ┴ ┴
doc └──┘ └──┘ └────┘ └─┘
542 begin
st └─────
543 apply eq_of_bisim (λc₁ c₂, c₁ = c₂ ∨
id └─────────┘ ┴ ┴
src └────┘└─────────┘┴ └─────┘ ┴┴┴ ┴┴└
typ └────┘└─────────┘┴ └─────┘ ┴┴┴ ┴┴└
doc └────┘ ┴ └─────┘ ┴ ┴ ┴ └
txt └────┘ ┴ └─────┘ ┴ ┴ ┴ └
par └────┘ ┴ └─────┘ ┴ ┴ ┴ └
pid ┴ ┴ └─────┘ ┴ ┴ ┴ └
st ───────────────────────────────────────
544 ∃ s, c₁ = bind s (return ∘ f) ∧ c₂ = map f s),
id ┴ ┴ └──┘ └────┘ ┴ ┴ └─┘ ┴
src ────────┘┴└┘┴┴ ┴ ┴└──┘┴ ┴ └────┘┴┴┴ └┘┴┴ ┴ ┴└─┘┴ ┴ ┴
typ ────────┘┴└┘┴┴ ┴ ┴└──┘┴ ┴ └────┘┴┴┴ └┘┴┴ ┴ ┴└─┘┴┴┴ ┴
doc ────────┘ └┘ ┴ ┴ ┴└──┘┴ ┴ └────┘┴ ┴ └┘ ┴ ┴ ┴└─┘┴ ┴ ┴
txt ────────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
par ────────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
pid ────────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────┘└─
545 { intros c₁ c₂ h,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └──────┘
st ───┘└────────────┘└─
546 exact match c₁, c₂, h with
id └┘ └┘ ┴
src └────┘ ┴ └┘ └┘ └─────
typ └────┘ ┴└┘└┘└┘└┘┴└─────
doc └────┘ ┴ └┘ └┘ └─────
txt └────┘ ┴ └┘ └┘ └─────
par └────┘ ┴ └┘ └┘ └─────
pid ┴ ┴ └┘ └┘ └─────
st ───────────────────────────────
547 | _, _, or.inl (eq.refl c) := begin cases destruct c with b cb; simp end
id └────┘ └─────┘ └──────┘ ┴
src ───────────┘└────┘┴ └─────┘┴ └───┘ ┴└────┘└──────┘┴ └────────┘└┘└───┘└───
typ ───────────┘└────┘┴ └─────┘┴ └───┘ ┴└────┘└──────┘┴┴└────────┘└┘└───┘└───
doc ───────────┘ ┴ ┴ └───┘ ┴└────┘└──────┘┴ └────────┘└┘└───┘└───
txt ───────────┘ ┴ ┴ └───┘ ┴└────┘ ┴ └────────┘└┘└───┘└───
par ───────────┘ ┴ ┴ └───┘ ┴└────┘ ┴ └────────┘└┘└───┘└───
pid ───────────┘ ┴ ┴ └───┘ └─────┘ ┴ └────────────────────
st ─────────────────────────────────┘└─────────────────────────────────────┘└─┘└
548 | _, _, or.inr ⟨s, rfl, rfl⟩ := begin
id └────┘ └─┘
src ───────────┘└────┘┴ └┘ └┘└─┘└───┘ └
typ ───────────┘└────┘┴ └┘ └┘└─┘└───┘ └
doc ───────────┘ ┴ └┘ └┘ └───┘ └
txt ───────────┘ ┴ └┘ └┘ └───┘ └
par ───────────┘ ┴ └┘ └┘ └───┘ └
pid ───────────┘ ┴ └┘ └┘ └───┘ └
st ───────────────────────────────────┘└─────
549 apply cases_on s; intros s; simp,
id └──────┘ ┴
src ─────┘└────┘└──────┘┴ └┘└──────┘└┘└──┘└─
typ ───────────┘└──────┘┴┴└┘└──────┘└┘└──┘└─
doc ─────┘└────┘ ┴ └┘└──────┘└┘└──┘└─
txt ─────┘└────┘ ┴ └┘└──────┘└┘└──┘└─
par ───────────┘ ┴ └┘└──────┘└┘└──┘└─
pid ───────────┘ ┴ └─────────────────
st ─────────────────────────────────────┘└─
550 exact or.inr ⟨s, rfl, rfl⟩
id └────┘ ┴ └─┘
src ───────────┘└────┘┴ └┘ └┘└─┘└─
typ ───────────┘└────┘┴ ┴└┘ └┘└─┘└─
doc ───────────┘ ┴ └┘ └┘ └─
txt ───────────┘ ┴ └┘ └┘ └─
par ───────────┘ ┴ └┘ └┘ └─
pid ───────────┘ ┴ └┘ └┘ └─
st ─────────────────────────────────
551 end end },
src ───────────┘
typ ───────────┘
doc ───────────┘
txt ───────────┘
par ───────────┘
pid ──────────┘┴
st ───┘└─┘└───┘└┘└
552 { exact or.inr ⟨s, rfl, rfl⟩ }
id └────┘ ┴ └─┘
src └────┘└────┘┴ └┘ └┘└─┘└┘
typ └────┘└────┘┴ ┴└┘ └┘└─┘└┘
doc └────┘ ┴ └┘ └┘ └┘
txt └────┘ ┴ └┘ └┘ └┘
par └────┘ ┴ └┘ └┘ └┘
pid ┴ ┴ └┘ └┘ ┴┴
st ──────────────────────────────┘└─
553 end
st ──┘
554
555 @[simp] theorem bind_ret' (s : computation α) : bind s return = s :=
id └─────────┘ ┴ └──┘ ┴ └────┘ ┴ ┴
src └─────────┘ └──┘ └────┘ ┴
typ └─────────┘ ┴ └──┘ ┴ └────┘ ┴ ┴
doc └──┘ └─────────┘ └──┘ └────┘
556 by rw bind_ret; change (λ x : α, x) with @id α; rw map_id
id └──────┘ ┴ └┘ ┴ └────┘
src └─┘└──────┘ └─────┘ └───┘ └┘ └─────┘ └┘┴ └─┘└────┘└
typ └─┘└──────┘ └─────┘ └───┘┴└┘ └─────┘ └┘┴┴ └─┘└────┘└
doc └─┘ └─────┘ └───┘ └┘ └─────┘ ┴ └─┘ └
txt └─┘ └─────┘ └───┘ └┘ └─────┘ ┴ └─┘ └
par └─┘ └─────┘ └───┘ └┘ └─────┘ ┴ └─┘ └
pid ┴ ┴ └───┘ └┘ ┴└────┘ ┴ ┴ └
st └───────────────────────────────────────────────┘└────┘└
557
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
558 @[simp] theorem bind_assoc (s : computation α) (f : α → computation β) (g : β → computation γ) :
id └─────────┘ ┴ ┴ └─────────┘ ┴ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘ └─────────┘
typ └─────────┘ ┴ ┴ └─────────┘ ┴ ┴ └─────────┘ ┴
doc └──┘ └─────────┘ └─────────┘ └─────────┘
559 bind (bind s f) g = bind s (λ (x : α), bind (f x) g) :=
id └──┘ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴
src └──┘ └──┘ ┴ └──┘ └──┘
typ └──┘ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──┘ └──┘ └──┘ └──┘
560 begin
st └─────
561 apply eq_of_bisim (λc₁ c₂, c₁ = c₂ ∨
id └─────────┘ ┴ ┴
src └────┘└─────────┘┴ └─────┘ ┴┴┴ ┴┴└
typ └────┘└─────────┘┴ └─────┘ ┴┴┴ ┴┴└
doc └────┘ ┴ └─────┘ ┴ ┴ ┴ └
txt └────┘ ┴ └─────┘ ┴ ┴ ┴ └
par └────┘ ┴ └─────┘ ┴ ┴ ┴ └
pid ┴ ┴ └─────┘ ┴ ┴ ┴ └
st ───────────────────────────────────────
562 ∃ s, c₁ = bind (bind s f) g ∧ c₂ = bind s (λ (x : α), bind (f x) g)),
id ┴ ┴ ┴ ┴ └──┘ ┴ ┴
src ────────┘┴└┘┴┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴┴ ┴ ┴ ┴ ┴ └────┘ └─┘└──┘┴ ┴ └┘ └┘
typ ────────┘┴└┘┴┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴┴ ┴ ┴ ┴ ┴ └────┘┴└─┘└──┘┴ ┴┴ └┘┴└┘
doc ────────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ └─┘└──┘┴ ┴ └┘ └┘
txt ────────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ └┘ └┘
par ────────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ └┘ └┘
pid ────────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ └┘ └┘
st ────────────────────────────────────────────────────────────────────────────┘└─
563 { intros c₁ c₂ h,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └──────┘
st ───┘└────────────┘└─
564 exact match c₁, c₂, h with
id └┘ └┘ ┴
src └────┘ ┴ └┘ └┘ └─────
typ └────┘ ┴└┘└┘└┘└┘┴└─────
doc └────┘ ┴ └┘ └┘ └─────
txt └────┘ ┴ └┘ └┘ └─────
par └────┘ ┴ └┘ └┘ └─────
pid ┴ ┴ └┘ └┘ └─────
st ───────────────────────────────
565 | _, _, or.inl (eq.refl c) := by cases destruct c with b cb; simp
id └────┘ └─────┘ └──────┘ ┴
src ───────────┘└────┘┴ └─────┘┴ └───┘ ┴└────┘└──────┘┴ └────────┘└┘└────
typ ───────────┘└────┘┴ └─────┘┴ └───┘ ┴└────┘└──────┘┴┴└────────┘└┘└────
doc ───────────┘ ┴ ┴ └───┘ ┴└────┘└──────┘┴ └────────┘└┘└────
txt ───────────┘ ┴ ┴ └───┘ ┴└────┘ ┴ └────────┘└┘└────
par ───────────┘ ┴ ┴ └───┘ ┴└────┘ ┴ └────────┘└┘└────
pid ───────────┘ ┴ ┴ └───┘ └─────┘ ┴ └────────────────
st ───────────────────────────────────┘└─────────────────────────────────
566 | ._, ._, or.inr ⟨s, rfl, rfl⟩ := begin
id └────┘ └─┘
src ───┘└┘ └┘ └┘└────┘┴ └┘ └┘└─┘└───┘ └
typ ───┘└┘ └┘ └┘└────┘┴ └┘ └┘└─┘└───┘ └
doc ───┘└┘ └┘ └┘ ┴ └┘ └┘ └───┘ └
txt ───┘└┘ └┘ └┘ ┴ └┘ └┘ └───┘ └
par ───┘└┘ └┘ └┘ ┴ └┘ └┘ └───┘ └
pid ─────┘ └┘ └┘ ┴ └┘ └┘ └───┘ └
st ───┘└────────────────────────────────┘└─────
567 apply cases_on s; intros s; simp,
id └──────┘ ┴
src ─────┘└────┘└──────┘┴ └┘└──────┘└┘└──┘└─
typ ───────────┘└──────┘┴┴└┘└──────┘└┘└──┘└─
doc ─────┘└────┘ ┴ └┘└──────┘└┘└──┘└─
txt ─────┘└────┘ ┴ └┘└──────┘└┘└──┘└─
par ───────────┘ ┴ └┘└──────┘└┘└──┘└─
pid ───────────┘ ┴ └─────────────────
st ─────────────────────────────────────┘└─
568 { generalize : f s = fs,
id ┴ ┴
src ───────┘└───────────┘ ┴ ┴ ┴ └─
typ ───────┘└───────────┘┴┴┴┴ ┴ └─
doc ───────┘└───────────┘ ┴ ┴ ┴ └─
txt ───────┘└───────────┘ ┴ ┴ ┴ └─
par ───────┘└───────────┘ ┴ ┴ ┴ └─
pid ────────────────────┘ ┴ ┴ ┴ └─
st ──────┘└────────────────────┘└─
569 apply cases_on fs; intros t; simp,
id └──────┘ └┘
src ───────┘└────┘└──────┘┴ └┘└──────┘└┘└──┘└─
typ ─────────────┘└──────┘┴└┘└┘└──────┘└┘└──┘└─
doc ───────┘└────┘ ┴ └┘└──────┘└┘└──┘└─
txt ───────┘└────┘ ┴ └┘└──────┘└┘└──┘└─
par ─────────────┘ ┴ └┘└──────┘└┘└──┘└─
pid ─────────────┘ ┴ └─────────────────
st ────────────────────────────────────────┘└─
570 { cases destruct (g t) with b cb; simp } },
id └──────┘ ┴ ┴
src ─────────┘└────┘└──────┘┴ ┴ └─────────┘└┘└───┘└────
typ ─────────┘└────┘└──────┘┴ ┴┴┴└─────────┘└┘└───┘└────
doc ─────────┘└────┘└──────┘┴ ┴ └─────────┘└┘└───┘└────
txt ─────────┘└────┘ ┴ ┴ └─────────┘└┘└───┘└────
par ─────────┘└────┘ ┴ ┴ └─────────┘└┘└───┘└────
pid ───────────────┘ ┴ ┴ └──────────────────────
st ──────────────────────────────────────────────┘└─┘└─
571 { exact or.inr ⟨s, rfl, rfl⟩ }
id └────┘ ┴ └─┘
src ─────────────┘└────┘┴ └┘ └┘└─┘└───
typ ─────────────┘└────┘┴ ┴└┘ └┘└─┘└───
doc ─────────────┘ ┴ └┘ └┘ └───
txt ─────────────┘ ┴ └┘ └┘ └───
par ─────────────┘ ┴ └┘ └┘ └───
pid ─────────────┘ ┴ └┘ └┘ └───
st ──────────────────────────────────┘└─
572 end end },
src ───────────┘
typ ───────────┘
doc ───────────┘
txt ───────────┘
par ───────────┘
pid ──────────┘┴
st ──────┘└───┘└┘└
573 { exact or.inr ⟨s, rfl, rfl⟩ }
id └────┘ ┴ └─┘
src └────┘└────┘┴ └┘ └┘└─┘└┘
typ └────┘└────┘┴ ┴└┘ └┘└─┘└┘
doc └────┘ ┴ └┘ └┘ └┘
txt └────┘ ┴ └┘ └┘ └┘
par └────┘ ┴ └┘ └┘ └┘
pid ┴ ┴ └┘ └┘ ┴┴
st ──────────────────────────────┘└─
574 end
st ──┘
575
576 theorem results_bind {s : computation α} {f : α → computation β} {a b m n}
id └─────────┘ ┴ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ └─────────┘ ┴ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
577 (h1 : results s a m) (h2 : results (f a) b n) : results (bind s f) b (n + m) :=
id └─────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ └─────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ └─────┘ └─────┘ └──┘ ┴
typ └─────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ └─────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ └─────┘ └─────┘ └──┘
578 begin
st └─────
579 have := h1.mem, revert m,
id └────┘
src └──────┘└────┘ └──────┘
typ └──────┘└────┘ └──────┘
doc └──────┘ └──────┘
txt └──────┘ └──────┘
par └──────┘ └──────┘
pid └───┘└─┘ └┘
st ───────────────┘└────────┘└─
580 apply mem_rec_on this _ (λ s IH, _); intros m h1,
id └────────┘ └──┘
src └────┘└────────┘┴ └─┘ └───────┘ └─────────┘
typ └────┘└────────┘┴└──┘└─┘ └───────┘ └─────────┘
doc └────┘ ┴ └─┘ └───────┘ └─────────┘
txt └────┘ ┴ └─┘ └───────┘ └─────────┘
par └────┘ ┴ └─┘ └───────┘ └─────────┘
pid ┴ ┴ └─┘ └───────┘ └───┘
st ─────────────────────────────────────────────────┘└─
581 { rw [ret_bind], rw h1.len_unique (results_ret _), exact h2 },
id └──────┘ └───────────┘ └─────────┘ └┘
src └──┘└──────┘┴ └─┘└───────────┘┴ └─────────┘└─┘ └────┘ ┴
typ └──┘└──────┘┴ └─┘└───────────┘┴ └─────────┘└─┘ └────┘└┘┴
doc └──┘ ┴ └─┘ ┴ └─┘ └────┘ ┴
txt └──┘ ┴ └─┘ ┴ └─┘ └────┘ ┴
par └──┘ ┴ └─┘ ┴ └─┘ └────┘ ┴
pid └┘ ┴ ┴ ┴ └─┘ ┴ ┴
st ───┘└──────────┘└─────────────────────────────────┘└─────────┘└┘└
582 { rw [think_bind], cases of_results_think h1 with m' h, cases h with h1 e,
id └────────┘ └──────────────┘ └┘ ┴
src └──┘└────────┘┴ └────┘└──────────────┘┴ └────────┘ └────┘ └────────┘
typ └──┘└────────┘┴ └────┘└──────────────┘┴└┘└────────┘ └────┘┴└────────┘
doc └──┘ ┴ └────┘ ┴ └────────┘ └────┘ └────────┘
txt └──┘ ┴ └────┘ ┴ └────────┘ └────┘ └────────┘
par └──┘ ┴ └────┘ ┴ └────────┘ └────┘ └────────┘
pid └┘ ┴ ┴ ┴ └────────┘ ┴ └────────┘
st ─────────────────┘└────────────────────────────────────┘└─────────────────┘└─
583 rw e, exact results_think (IH h1) }
id ┴ └───────────┘ └┘ └┘
src └─┘ └────┘└───────────┘┴ ┴ └┘
typ └─┘┴ └────┘└───────────┘┴ └┘┴└┘└┘
doc └─┘ └────┘ ┴ ┴ └┘
txt └─┘ └────┘ ┴ ┴ └┘
par └─┘ └────┘ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴┴
st ───────┘└────────────────────────────┘└─
584 end
st ──┘
585
586 theorem mem_bind {s : computation α} {f : α → computation β} {a b}
id └─────────┘ ┴ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ └─────────┘ ┴ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
587 (h1 : a ∈ s) (h2 : b ∈ f a) : b ∈ bind s f :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
src ┴ ┴ ┴ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
doc └──┘
588 let ⟨m, h1⟩ := exists_results_of_mem h1,
id └─┘ └┘ └───────────────────┘ └┘
src └───────────────────┘
typ └─┘ └┘ └───────────────────┘ └┘
589 ⟨n, h2⟩ := exists_results_of_mem h2 in (results_bind h1 h2).mem
id └┘ └───────────────────┘ └┘ └──────────┘ └─┘
src └───────────────────┘ └──────────┘ └─┘
typ └┘ └───────────────────┘ └┘ └──────────┘ └─┘
590
591 instance terminates_bind (s : computation α) (f : α → computation β)
id └─────────┘ ┴ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ └─────────┘ ┴ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
592 [terminates s] [terminates (f (get s))] :
id └────────┘ ┴ └────────┘ ┴ └─┘ ┴
src └────────┘ └────────┘ └─┘
typ └────────┘ ┴ └────────┘ ┴ └─┘ ┴
doc └────────┘ └────────┘ └─┘
593 terminates (bind s f) :=
id └────────┘ └──┘ ┴ ┴
src └────────┘ └──┘
typ └────────┘ └──┘ ┴ ┴
doc └────────┘ └──┘
594 terminates_of_mem (mem_bind (get_mem s) (get_mem (f (get s))))
id └───────────────┘ └──────┘ └─────┘ ┴ └─────┘ ┴ └─┘ ┴
src └───────────────┘ └──────┘ └─────┘ └─────┘ └─┘
typ └───────────────┘ └──────┘ └─────┘ ┴ └─────┘ ┴ └─┘ ┴
doc └─┘
595
596 @[simp] theorem get_bind (s : computation α) (f : α → computation β)
id └─────────┘ ┴ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ └─────────┘ ┴ ┴ └─────────┘ ┴
doc └──┘ └─────────┘ └─────────┘
597 [terminates s] [terminates (f (get s))] :
id └────────┘ ┴ └────────┘ ┴ └─┘ ┴
src └────────┘ └────────┘ └─┘
typ └────────┘ ┴ └────────┘ ┴ └─┘ ┴
doc └────────┘ └────────┘ └─┘
598 get (bind s f) = get (f (get s)) :=
id └─┘ └──┘ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴
src └─┘ └──┘ ┴ └─┘ └─┘
typ └─┘ └──┘ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴
doc └─┘ └──┘ └─┘ └─┘
599 get_eq_of_mem _ (mem_bind (get_mem s) (get_mem (f (get s))))
id └───────────┘ └──────┘ └─────┘ ┴ └─────┘ ┴ └─┘ ┴
src └───────────┘ └──────┘ └─────┘ └─────┘ └─┘
typ └───────────┘ └──────┘ └─────┘ ┴ └─────┘ ┴ └─┘ ┴
doc └─┘
600
601 @[simp] theorem length_bind (s : computation α) (f : α → computation β)
id └─────────┘ ┴ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ └─────────┘ ┴ ┴ └─────────┘ ┴
doc └──┘ └─────────┘ └─────────┘
602 [T1 : terminates s] [T2 : terminates (f (get s))] :
id └────────┘ ┴ └────────┘ ┴ └─┘ ┴
src └────────┘ └────────┘ └─┘
typ └────────┘ ┴ └────────┘ ┴ └─┘ ┴
doc └────────┘ └────────┘ └─┘
603 length (bind s f) = length (f (get s)) + length s :=
id └────┘ └──┘ ┴ ┴ ┴ └────┘ ┴ └─┘ ┴ ┴ └────┘ ┴
src └────┘ └──┘ ┴ └────┘ └─┘ ┴ └────┘
typ └────┘ └──┘ ┴ ┴ ┴ └────┘ ┴ └─┘ ┴ ┴ └────┘ ┴
doc └────┘ └──┘ └────┘ └─┘ └────┘
604 (results_of_terminates _).len_unique $
id └───────────────────┘ └────────┘
src └───────────────────┘ └────────┘
typ └───────────────────┘ └────────┘
605 results_bind (results_of_terminates _) (results_of_terminates _)
id └──────────┘ └───────────────────┘ └───────────────────┘
src └──────────┘ └───────────────────┘ └───────────────────┘
typ └──────────┘ └───────────────────┘ └───────────────────┘
606
607 theorem of_results_bind {s : computation α} {f : α → computation β} {b k} :
id └─────────┘ ┴ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ └─────────┘ ┴ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
608 results (bind s f) b k →
id └─────┘ └──┘ ┴ ┴ ┴ ┴
src └─────┘ └──┘
typ └─────┘ └──┘ ┴ ┴ ┴ ┴
doc └─────┘ └──┘
609 ∃ a m n, results s a m ∧ results (f a) b n ∧ k = n + m :=
id ┴ ┴ ┴ ┴┴ └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └─────┘ ┴ └─────┘ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴ └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ └─────┘
610 begin
st └─────
611 induction k with n IH generalizing s;
id ┴
src └────────┘ └───────────────────────┘
typ └────────┘┴└───────────────────────┘
doc └────────┘ └───────────────────────┘
txt └────────┘ └───────────────────────┘
par └────────┘ └───────────────────────┘
pid ┴ ┴└───────┘└─────────────┘
st ────────────────────────────────────────
612 apply cases_on s (λ a, _) (λ s', _); intro e,
id └──────┘ ┴
src └────┘└──────┘┴ ┴ └─────┘ └─────┘ └─────┘
typ └────┘└──────┘┴┴┴ └─────┘ └─────┘ └─────┘
doc └────┘ ┴ ┴ └─────┘ └─────┘ └─────┘
txt └────┘ ┴ ┴ └─────┘ └─────┘ └─────┘
par └────┘ ┴ ┴ └─────┘ └─────┘ └─────┘
pid ┴ ┴ ┴ └─────┘ └─────┘ └┘
st ─────────────────────────────────────────────┘└─
613 { simp [thinkN] at e, refine ⟨a, _, _, results_ret _, e, rfl⟩ },
id └────┘ ┴ └─────────┘ ┴ └─┘
src └────┘└────┘└────┘ └─────┘ └──────┘└─────────┘└──┘ └┘└─┘└┘
typ └────┘└────┘└────┘ └─────┘ ┴└──────┘└─────────┘└──┘┴└┘└─┘└┘
doc └────┘└────┘└────┘ └─────┘ └──────┘ └──┘ └┘ └┘
txt └────┘ └────┘ └─────┘ └──────┘ └──┘ └┘ └┘
par └────┘ └────┘ └─────┘ └──────┘ └──┘ └┘ └┘
pid ┴┴ ┴┴└──┘ ┴ └──────┘ └──┘ └┘ ┴┴
st ───┘└────────────────┘└────────────────────────────────────────┘└┘└
614 { have := congr_arg head (eq_thinkN e), contradiction },
id └───────┘ └──┘ └───────┘ ┴
src └──────┘└───────┘┴└──┘┴ └───────┘┴ ┴ └────────────┘
typ └──────┘└───────┘┴└──┘┴ └───────┘┴┴┴ └────────────┘
doc └──────┘ ┴└──┘┴ ┴ ┴ └────────────┘
txt └──────┘ ┴ ┴ ┴ ┴ └────────────┘
par └──────┘ ┴ ┴ ┴ ┴ └────────────┘
pid └───┘└─┘ ┴ ┴ ┴ ┴ ┴
st ───┘└──────────────────────────────────┘└──────────────┘└┘└
615 { simp at e, refine ⟨a, _, n+1, results_ret _, e, rfl⟩ },
id ┴ ┴┴ └─────────┘ ┴ └─┘
src └───────┘ └─────┘ └───┘ ┴└─┘└─────────┘└──┘ └┘└─┘└┘
typ └───────┘ └─────┘ ┴└───┘┴┴└─┘└─────────┘└──┘┴└┘└─┘└┘
doc └───────┘ └─────┘ └───┘ └─┘ └──┘ └┘ └┘
txt └───────┘ └─────┘ └───┘ └─┘ └──┘ └┘ └┘
par └───────┘ └─────┘ └───┘ └─┘ └──┘ └┘ └┘
pid ┴└──┘ ┴ └───┘ └─┘ └──┘ └┘ ┴┴
st ───┘└───────┘└──────────────────────────────────────────┘└┘└
616 { simp at e, exact let ⟨a, m, n', h1, h2, e'⟩ := IH e in
id └┘ ┴
src └───────┘ └────┘ ┴ └┘ └┘ └┘ └┘ └┘ └───┘ ┴ └───
typ └───────┘ └────┘ ┴ └┘ └┘ └┘ └┘ └┘ └───┘└┘┴┴└───
doc └───────┘ └────┘ ┴ └┘ └┘ └┘ └┘ └┘ └───┘ ┴ └───
txt └───────┘ └────┘ ┴ └┘ └┘ └┘ └┘ └┘ └───┘ ┴ └───
par └───────┘ └────┘ ┴ └┘ └┘ └┘ └┘ └┘ └───┘ ┴ └───
pid ┴└──┘ ┴ ┴ └┘ └┘ └┘ └┘ └┘ └───┘ ┴ └───
st ────────────┘└─────────────────────────────────────────────
617 by rw e'; exact ⟨a, m.succ, n', results_think h1, h2, rfl⟩ }
id └┘ ┴ └────┘ └┘ └───────────┘ └┘ └┘ └─┘
src ───┘ ┴└─┘ └──────┘ └┘└────┘└┘ └┘└───────────┘┴ └┘ └┘└─┘└┘
typ ───┘ ┴└─┘└┘└──────┘ ┴└┘└────┘└┘└┘└┘└───────────┘┴└┘└┘└┘└┘└─┘└┘
doc ───┘ ┴└─┘ └──────┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘
txt ───┘ ┴└─┘ └──────┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘
par ───┘ ┴└─┘ └──────┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘
pid ───┘ └──┘ └──────┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘
st ─────┘└───────────────────────────────────────────────────────┘└─
618 end
st ──┘
619
620 theorem exists_of_mem_bind {s : computation α} {f : α → computation β} {b}
id └─────────┘ ┴ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ └─────────┘ ┴ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
621 (h : b ∈ bind s f) : ∃ a ∈ s, b ∈ f a :=
id ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ └──┘ ┴ ┴ ┴
typ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc └──┘
622 let ⟨k, h⟩ := exists_results_of_mem h,
id └─┘ ┴ └───────────────────┘ ┴
src └───────────────────┘
typ └─┘ ┴ └───────────────────┘ ┴
623 ⟨a, m, n, h1, h2, e⟩ := of_results_bind h in ⟨a, h1.mem, h2.mem⟩
id ┴ └┘ └┘ └─────────────┘ └──┘ └──┘
src └─────────────┘ └──┘ └──┘
typ ┴ └┘ └┘ └─────────────┘ └──┘ └──┘
624
625 theorem bind_promises {s : computation α} {f : α → computation β} {a b}
id └─────────┘ ┴ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ └─────────┘ ┴ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
626 (h1 : s ~> a) (h2 : f a ~> b) : bind s f ~> b :=
id ┴ └┘ ┴ ┴ ┴ └┘ ┴ └──┘ ┴ ┴ └┘ ┴
src └┘ └┘ └──┘ └┘
typ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └──┘ ┴ ┴ └┘ ┴
doc └┘ └┘ └──┘ └┘
627 λ b' bB, begin
id └┘ └┘
typ └┘ └┘
st └─────
628 rcases exists_of_mem_bind bB with ⟨a', a's, ba'⟩,
id └────────────────┘ └┘
src └─────┘└────────────────┘┴ └──────────────────┘
typ └─────┘└────────────────┘┴└┘└──────────────────┘
doc └─────┘ ┴ └──────────────────┘
txt └─────┘ ┴ └──────────────────┘
par └─────┘ ┴ └──────────────────┘
pid ┴ ┴ └──────────────────┘
st ─────────────────────────────────────────────────┘└─
629 rw ←h1 a's at ba', exact h2 ba'
id └┘ └─┘ └┘ └─┘
src └──┘ ┴ └─────┘ └────┘ ┴ ┴
typ └──┘└┘┴└─┘└─────┘ └────┘└┘┴└─┘┴
doc └──┘ ┴ └─────┘ └────┘ ┴ ┴
txt └──┘ ┴ └─────┘ └────┘ ┴ ┴
par └──┘ ┴ └─────┘ └────┘ ┴ ┴
pid └┘ ┴ └─────┘ ┴ ┴ ┴
st ──────────────────┘└─────────────┘
630 end
st └─┘
631
632 instance : monad computation :=
id └───┘ └─────────┘
src └───┘ └─────────┘
typ └───┘ └─────────┘
doc └─────────┘
633 { map := @map,
id └─┘
src └─┘
typ └─┘
doc └─┘
634 pure := @return,
id └────┘
src └────┘
typ └────┘
doc └────┘
635 bind := @bind }
id └──┘
src └──┘
typ └──┘
doc └──┘
636
637 instance : is_lawful_monad computation :=
id └─────────────┘ └─────────┘
src └─────────────┘ └─────────┘
typ └─────────────┘ └─────────┘
doc └─────────┘
638 { id_map := @map_id,
id ┴ └────┘
src ┴ └────┘
typ ┴ └────┘
639 bind_pure_comp_eq_map := @bind_ret,
id └──────┘
src └──────┘
typ └──────┘
640 pure_bind := @ret_bind,
id └──────┘
src └──────┘
typ └──────┘
641 bind_assoc := @bind_assoc }
id └────────┘
src └────────┘
typ └────────┘
642
643 theorem has_map_eq_map {β} (f : α → β) (c : computation α) : f <$> c = map f c := rfl
id ┴ ┴ └─────────┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘
src └─────────┘ └─┘ ┴ └─┘ └─┘
typ ┴ ┴ └─────────┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘
doc └─────────┘ └─┘
644
645 @[simp] theorem return_def (a) : (_root_.return a : computation α) = return a := rfl
id └───────────┘ ┴ └─────────┘ ┴ ┴ └────┘ ┴ └─┘
src └───────────┘ └─────────┘ ┴ └────┘ └─┘
typ └───────────┘ ┴ └─────────┘ ┴ ┴ └────┘ ┴ └─┘
doc └──┘ └─────────┘ └────┘
646
647 @[simp] theorem map_ret' {α β} : ∀ (f : α → β) (a), f <$> return a = return (f a) := map_ret
id ┴ ┴ ┴ ┴ ┴ └─┘ └────┘ ┴ ┴ └────┘ ┴ ┴ └─────┘
src └─┘ └────┘ ┴ └────┘ └─────┘
typ ┴ ┴ ┴ ┴ ┴ └─┘ └────┘ ┴ ┴ └────┘ ┴ ┴ └─────┘
doc └──┘ └────┘ └────┘
648 @[simp] theorem map_think' {α β} : ∀ (f : α → β) s, f <$> think s = think (f <$> s) := map_think
id ┴ ┴ ┴ ┴ ┴ └─┘ └───┘ ┴ ┴ └───┘ ┴ └─┘ ┴ └───────┘
src └─┘ └───┘ ┴ └───┘ └─┘ └───────┘
typ ┴ ┴ ┴ ┴ ┴ └─┘ └───┘ ┴ ┴ └───┘ ┴ └─┘ ┴ └───────┘
doc └──┘ └───┘ └───┘
649
650 theorem mem_map (f : α → β) {a} {s : computation α} (m : a ∈ s) : f a ∈ map f s :=
id ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
src └─────────┘ ┴ ┴ └─┘
typ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
doc └─────────┘ └─┘
651 by rw ←bind_ret; apply mem_bind m; apply ret_mem
id └──────┘ └──────┘ ┴ └─────┘
src └──┘└──────┘ └────┘└──────┘┴ └────┘└─────┘└
typ └──┘└──────┘ └────┘└──────┘┴┴ └────┘└─────┘└
doc └──┘ └────┘ ┴ └────┘ └
txt └──┘ └────┘ ┴ └────┘ └
par └──┘ └────┘ ┴ └────┘ └
pid └┘ ┴ ┴ ┴ └
st └──────────────────────────────────────────────
652
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
653 theorem exists_of_mem_map {f : α → β} {b : β} {s : computation α} (h : b ∈ map f s) :
id ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ └─┘ ┴ ┴
src └─────────┘ ┴ └─┘
typ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ └─┘ ┴ ┴
doc └─────────┘ └─┘
654 ∃ a, a ∈ s ∧ f a = b :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
655 by rw ←bind_ret at h; exact
id └──────┘
src └──┘└──────┘└───┘ └────┘
typ └──┘└──────┘└───┘ └────┘
doc └──┘ └───┘ └────┘
txt └──┘ └───┘ └────┘
par └──┘ └───┘ └────┘
pid └┘ └───┘ ┴
st └─────────────────────────
656 let ⟨a, as, fb⟩ := exists_of_mem_bind h in ⟨a, as, mem_unique (ret_mem _) fb⟩
id ┴ └┘ └┘ └────────────────┘ ┴ └────────┘ └─────┘
src ┴ └┘ └┘ └───┘└────────────────┘┴ └──┘ └┘ └┘└────────┘┴ └─────┘└──┘ └─
typ ┴ ┴└┘└┘└┘└┘└───┘└────────────────┘┴┴└──┘ └┘ └┘└────────┘┴ └─────┘└──┘ └─
doc ┴ └┘ └┘ └───┘ ┴ └──┘ └┘ └┘ ┴ └──┘ └─
txt ┴ └┘ └┘ └───┘ ┴ └──┘ └┘ └┘ ┴ └──┘ └─
par ┴ └┘ └┘ └───┘ ┴ └──┘ └┘ └┘ ┴ └──┘ └─
pid ┴ └┘ └┘ └───┘ ┴ └──┘ └┘ └┘ ┴ └──┘ ┴└
st ──────────────────────────────────────────────────────────────────────────────
657
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
658 instance terminates_map (f : α → β) (s : computation α) [terminates s] : terminates (map f s) :=
id ┴ ┴ └─────────┘ ┴ └────────┘ ┴ └────────┘ └─┘ ┴ ┴
src └─────────┘ └────────┘ └────────┘ └─┘
typ ┴ ┴ └─────────┘ ┴ └────────┘ ┴ └────────┘ └─┘ ┴ ┴
doc └─────────┘ └────────┘ └────────┘ └─┘
659 by rw ←bind_ret; apply_instance
id └──────┘
src └──┘└──────┘ └──────────────
typ └──┘└──────┘ └──────────────
doc └──┘ └──────────────
txt └──┘ └──────────────
par └──┘ └──────────────
pid └┘ └
st └─────────────────────────────
660
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
661 theorem terminates_map_iff (f : α → β) (s : computation α) :
id ┴ ┴ └─────────┘ ┴
src └─────────┘
typ ┴ ┴ └─────────┘ ┴
doc └─────────┘
662 terminates (map f s) ↔ terminates s :=
id └────────┘ └─┘ ┴ ┴ ┴ └────────┘ ┴
src └────────┘ └─┘ ┴ └────────┘
typ └────────┘ └─┘ ┴ ┴ ┴ └────────┘ ┴
doc └────────┘ └─┘ └────────┘
663 ⟨λ⟨a, h⟩, let ⟨b, h1, _⟩ := exists_of_mem_map h in ⟨_, h1⟩, @computation.terminates_map _ _ _ _⟩
id ┴ ┴ └─┘ └┘ └───────────────┘ └────────────────────────┘
src └───────────────┘ └────────────────────────┘
typ ┴ ┴ └─┘ └┘ └───────────────┘ └────────────────────────┘
664
665 -- Parallel computation
666 /-- `c₁ <|> c₂` calculates `c₁` and `c₂` simultaneously, returning
667 the first one that gives a result. -/
668 def orelse (c₁ c₂ : computation α) : computation α :=
id └─────────┘ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ └─────────┘ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
669 @computation.corec α (computation α × computation α)
id └───────────────┘ ┴ └─────────┘ ┴ ┴ └─────────┘ ┴
src └───────────────┘ └─────────┘ ┴ └─────────┘
typ └───────────────┘ ┴ └─────────┘ ┴ ┴ └─────────┘ ┴
doc └───────────────┘ └─────────┘ └─────────┘
670 (λ⟨c₁, c₂⟩, match destruct c₁ with
id ┴└┘ └┘ └──────┘
src └──────┘
typ ┴└┘ └┘ └──────┘
doc └──────┘
671 | sum.inl a := sum.inl a
id └─────┘ ┴ └─────┘
src └─────┘ └─────┘
typ └─────┘ ┴ └─────┘
672 | sum.inr c₁' := match destruct c₂ with
id └─────┘ └─┘ └──────┘
src └─────┘ └──────┘
typ └─────┘ └─┘ └──────┘
doc └──────┘
673 | sum.inl a := sum.inl a
id └─────┘ ┴ └─────┘
src └─────┘ └─────┘
typ └─────┘ ┴ └─────┘
674 | sum.inr c₂' := sum.inr (c₁', c₂')
id └─────┘ └─┘ └─────┘ ┴
src └─────┘ └─────┘ ┴
typ └─────┘ └─┘ └─────┘ ┴
675 end
676 end) (c₁, c₂)
id ┴└┘ └┘
src ┴
typ ┴└┘ └┘
677
678 instance : alternative computation :=
id └─────────┘ └─────────┘
src └─────────┘ └─────────┘
typ └─────────┘ └─────────┘
doc └─────────┘
679 { orelse := @orelse, failure := @empty, ..computation.monad }
id └────┘ └───┘ └───────────────┘
src └────┘ └───┘ └───────────────┘
typ └────┘ └───┘ └───────────────┘
doc └────┘ └───┘
680
681 @[simp] theorem ret_orelse (a : α) (c₂ : computation α) :
id ┴ └─────────┘ ┴
src └─────────┘
typ ┴ └─────────┘ ┴
doc └──┘ └─────────┘
682 (return a <|> c₂) = return a :=
id └────┘ ┴ └─┘ └┘ ┴ └────┘ ┴
src └────┘ └─┘ ┴ └────┘
typ └────┘ ┴ └─┘ └┘ ┴ └────┘ ┴
doc └────┘ └────┘
683 destruct_eq_ret $ by unfold has_orelse.orelse; simp [orelse]
id └─────────────┘ └────┘
src └─────────────┘ └──────────────────────┘ └────┘└────┘└─
typ └─────────────┘ └──────────────────────┘ └────┘└────┘└─
doc └──────────────────────┘ └────┘└────┘└─
txt └──────────────────────┘ └────┘ └─
par └──────────────────────┘ └────┘ └─
pid └────────────────┘ ┴┴ ┴└
st └────────────────────────────────────────
684
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
685 @[simp] theorem orelse_ret (c₁ : computation α) (a : α) :
id └─────────┘ ┴ ┴
src └─────────┘
typ └─────────┘ ┴ ┴
doc └──┘ └─────────┘
686 (think c₁ <|> return a) = return a :=
id └───┘ └┘ └─┘ └────┘ ┴ ┴ └────┘ ┴
src └───┘ └─┘ └────┘ ┴ └────┘
typ └───┘ └┘ └─┘ └────┘ ┴ ┴ └────┘ ┴
doc └───┘ └────┘ └────┘
687 destruct_eq_ret $ by unfold has_orelse.orelse; simp [orelse]
id └─────────────┘ └────┘
src └─────────────┘ └──────────────────────┘ └────┘└────┘└─
typ └─────────────┘ └──────────────────────┘ └────┘└────┘└─
doc └──────────────────────┘ └────┘└────┘└─
txt └──────────────────────┘ └────┘ └─
par └──────────────────────┘ └────┘ └─
pid └────────────────┘ ┴┴ ┴└
st └────────────────────────────────────────
688
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
689 @[simp] theorem orelse_think (c₁ c₂ : computation α) :
id └─────────┘ ┴
src └─────────┘
typ └─────────┘ ┴
doc └──┘ └─────────┘
690 (think c₁ <|> think c₂) = think (c₁ <|> c₂) :=
id └───┘ └┘ └─┘ └───┘ └┘ ┴ └───┘ └┘ └─┘ └┘
src └───┘ └─┘ └───┘ ┴ └───┘ └─┘
typ └───┘ └┘ └─┘ └───┘ └┘ ┴ └───┘ └┘ └─┘ └┘
doc └───┘ └───┘ └───┘
691 destruct_eq_think $ by unfold has_orelse.orelse; simp [orelse]
id └───────────────┘ └────┘
src └───────────────┘ └──────────────────────┘ └────┘└────┘└─
typ └───────────────┘ └──────────────────────┘ └────┘└────┘└─
doc └──────────────────────┘ └────┘└────┘└─
txt └──────────────────────┘ └────┘ └─
par └──────────────────────┘ └────┘ └─
pid └────────────────┘ ┴┴ ┴└
st └────────────────────────────────────────
692
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
693 @[simp] theorem empty_orelse (c) : (empty α <|> c) = c :=
id └───┘ ┴ └─┘ ┴ ┴ ┴
src └───┘ └─┘ ┴
typ └───┘ ┴ └─┘ ┴ ┴ ┴
doc └──┘ └───┘
694 begin
st └─────
695 apply eq_of_bisim (λc₁ c₂, (empty α <|> c₂) = c₁) _ rfl,
id └─────────┘ └───┘ ┴ └─┘ ┴ └─┘
src └────┘└─────────┘┴ └─────┘ └───┘┴ ┴└─┘┴ └┘┴┴ └──┘└─┘
typ └────┘└─────────┘┴ └─────┘ └───┘┴┴┴└─┘┴ └┘┴┴ └──┘└─┘
doc └────┘ ┴ └─────┘ └───┘┴ ┴ ┴ └┘ ┴ └──┘
txt └────┘ ┴ └─────┘ ┴ ┴ ┴ └┘ ┴ └──┘
par └────┘ ┴ └─────┘ ┴ ┴ ┴ └┘ ┴ └──┘
pid ┴ ┴ └─────┘ ┴ ┴ ┴ └┘ ┴ └──┘
st ────────────────────────────────────────────────────────┘└─
696 intros s' s h, rw ←h,
id ┴
src └───────────┘ └──┘
typ └───────────┘ └──┘┴
doc └───────────┘ └──┘
txt └───────────┘ └──┘
par └───────────┘ └──┘
pid └─────┘ └┘
st ──────────────┘└─────┘└─
697 apply cases_on s; intros s; rw think_empty; simp,
id └──────┘ ┴ └─────────┘
src └────┘└──────┘┴ └──────┘ └─┘└─────────┘ └──┘
typ └────┘└──────┘┴┴ └──────┘ └─┘└─────────┘ └──┘
doc └────┘ ┴ └──────┘ └─┘ └──┘
txt └────┘ ┴ └──────┘ └─┘ └──┘
par └────┘ ┴ └──────┘ └─┘ └──┘
pid ┴ ┴ └┘ ┴
st ────────────────────────────────┘└─────────┘└────┘└─
698 rw ←think_empty,
id └─────────┘
src └──┘└─────────┘
typ └──┘└─────────┘
doc └──┘
txt └──┘
par └──┘
pid └┘
st ────────────────┘└─
699 end
st ──┘
700
701 @[simp] theorem orelse_empty (c : computation α) : (c <|> empty α) = c :=
id └─────────┘ ┴ ┴ └─┘ └───┘ ┴ ┴ ┴
src └─────────┘ └─┘ └───┘ ┴
typ └─────────┘ ┴ ┴ └─┘ └───┘ ┴ ┴ ┴
doc └──┘ └─────────┘ └───┘
702 begin
st └─────
703 apply eq_of_bisim (λc₁ c₂, (c₂ <|> empty α) = c₁) _ rfl,
id └─────────┘ └─┘ └───┘ ┴ ┴ └─┘
src └────┘└─────────┘┴ └─────┘ ┴└─┘┴└───┘┴ └┘┴┴ └──┘└─┘
typ └────┘└─────────┘┴ └─────┘ ┴└─┘┴└───┘┴┴└┘┴┴ └──┘└─┘
doc └────┘ ┴ └─────┘ ┴ ┴└───┘┴ └┘ ┴ └──┘
txt └────┘ ┴ └─────┘ ┴ ┴ ┴ └┘ ┴ └──┘
par └────┘ ┴ └─────┘ ┴ ┴ ┴ └┘ ┴ └──┘
pid ┴ ┴ └─────┘ ┴ ┴ ┴ └┘ ┴ └──┘
st ────────────────────────────────────────────────────────┘└─
704 intros s' s h, rw ←h,
id ┴
src └───────────┘ └──┘
typ └───────────┘ └──┘┴
doc └───────────┘ └──┘
txt └───────────┘ └──┘
par └───────────┘ └──┘
pid └─────┘ └┘
st ──────────────┘└─────┘└─
705 apply cases_on s; intros s; rw think_empty; simp,
id └──────┘ ┴ └─────────┘
src └────┘└──────┘┴ └──────┘ └─┘└─────────┘ └──┘
typ └────┘└──────┘┴┴ └──────┘ └─┘└─────────┘ └──┘
doc └────┘ ┴ └──────┘ └─┘ └──┘
txt └────┘ ┴ └──────┘ └─┘ └──┘
par └────┘ ┴ └──────┘ └─┘ └──┘
pid ┴ ┴ └┘ ┴
st ────────────────────────────────┘└─────────┘└────┘└─
706 rw←think_empty,
id └─────────┘
src └─┘└─────────┘
typ └─┘└─────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────────────┘└─
707 end
st ──┘
708
709 /-- `c₁ ~ c₂` asserts that `c₁` and `c₂` either both terminate with the same result,
710 or both loop forever. -/
711 def equiv (c₁ c₂ : computation α) : Prop := ∀ a, a ∈ c₁ ↔ a ∈ c₂
id └─────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘
src └─────────┘ ┴ ┴ ┴
typ └─────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘
doc └─────────┘
712
713 infix ~ := equiv
id └───┘
src └───┘
typ └───┘
doc └───┘
714
715 @[refl] theorem equiv.refl (s : computation α) : s ~ s := λ_, iff.rfl
id └─────────┘ ┴ ┴ ┴ ┴ ┴ └─────┘
src └──┘ └─────────┘ ┴ └─────┘
typ └─────────┘ ┴ ┴ ┴ ┴ ┴ └─────┘
doc └──┘ └─────────┘ ┴
716
717 @[symm] theorem equiv.symm {s t : computation α} : s ~ t → t ~ s :=
id └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ └─────────┘ ┴ ┴
typ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └─────────┘ ┴ ┴
718 λh a, (h a).symm
id ┴ ┴ ┴ ┴ └──┘
src └──┘
typ ┴ ┴ ┴ ┴ └──┘
719
720 @[trans] theorem equiv.trans {s t u : computation α} : s ~ t → t ~ u → s ~ u :=
id └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ └─────────┘ ┴ ┴ ┴
typ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘ └─────────┘ ┴ ┴ ┴
721 λh1 h2 a, (h1 a).trans (h2 a)
id └┘ └┘ ┴ └┘ ┴ └───┘ └┘ ┴
src └───┘
typ └┘ └┘ ┴ └┘ ┴ └───┘ └┘ ┴
722
723 theorem equiv.equivalence : equivalence (@equiv α) :=
id └─────────┘ └───┘ ┴
src └─────────┘ └───┘
typ └─────────┘ └───┘ ┴
doc └───┘
724 ⟨@equiv.refl _, @equiv.symm _, @equiv.trans _⟩
id └────────┘ └────────┘ └─────────┘
src └────────┘ └────────┘ └─────────┘
typ └────────┘ └────────┘ └─────────┘
725
726 theorem equiv_of_mem {s t : computation α} {a} (h1 : a ∈ s) (h2 : a ∈ t) : s ~ t :=
id └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────┘ ┴ ┴ ┴
typ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────────┘ ┴
727 λa', ⟨λma, by rw mem_unique ma h1; exact h2,
id └┘ └┘ └────────┘ └┘ └┘ └┘
src └─┘└────────┘┴ ┴ └────┘
typ └┘ └┘ └─┘└────────┘┴└┘┴└┘ └────┘└┘
doc └─┘ ┴ ┴ └────┘
txt └─┘ ┴ ┴ └────┘
par └─┘ ┴ ┴ └────┘
pid ┴ ┴ ┴ ┴
st └────────────────────────────┘
728 λma, by rw mem_unique ma h2; exact h1⟩
id └┘ └────────┘ └┘ └┘ └┘
src └─┘└────────┘┴ ┴ └────┘
typ └┘ └─┘└────────┘┴└┘┴└┘ └────┘└┘
doc └─┘ ┴ ┴ └────┘
txt └─┘ ┴ ┴ └────┘
par └─┘ ┴ ┴ └────┘
pid ┴ ┴ ┴ ┴
st └────────────────────────────┘
729
730 theorem terminates_congr {c₁ c₂ : computation α}
id └─────────┘ ┴
src └─────────┘
typ └─────────┘ ┴
doc └─────────┘
731 (h : c₁ ~ c₂) : terminates c₁ ↔ terminates c₂ :=
id └┘ ┴ └┘ └────────┘ └┘ ┴ └────────┘ └┘
src ┴ └────────┘ ┴ └────────┘
typ └┘ ┴ └┘ └────────┘ └┘ ┴ └────────┘ └┘
doc ┴ └────────┘ └────────┘
732 exists_congr h
id └──────────┘ ┴
src └──────────┘
typ └──────────┘ ┴
733
734 theorem promises_congr {c₁ c₂ : computation α}
id └─────────┘ ┴
src └─────────┘
typ └─────────┘ ┴
doc └─────────┘
735 (h : c₁ ~ c₂) (a) : c₁ ~> a ↔ c₂ ~> a :=
id └┘ ┴ └┘ └┘ └┘ ┴ ┴ └┘ └┘ ┴
src ┴ └┘ ┴ └┘
typ └┘ ┴ └┘ └┘ └┘ ┴ ┴ └┘ └┘ ┴
doc ┴ └┘ └┘
736 forall_congr (λa', imp_congr (h a') iff.rfl)
id └──────────┘ └┘ └───────┘ ┴ └┘ └─────┘
src └──────────┘ └───────┘ └─────┘
typ └──────────┘ └┘ └───────┘ ┴ └┘ └─────┘
737
738 theorem get_equiv {c₁ c₂ : computation α} (h : c₁ ~ c₂)
id └─────────┘ ┴ └┘ ┴ └┘
src └─────────┘ ┴
typ └─────────┘ ┴ └┘ ┴ └┘
doc └─────────┘ ┴
739 [terminates c₁] [terminates c₂] : get c₁ = get c₂ :=
id └────────┘ └┘ └────────┘ └┘ └─┘ └┘ ┴ └─┘ └┘
src └────────┘ └────────┘ └─┘ ┴ └─┘
typ └────────┘ └┘ └────────┘ └┘ └─┘ └┘ ┴ └─┘ └┘
doc └────────┘ └────────┘ └─┘ └─┘
740 get_eq_of_mem _ $ (h _).2 $ get_mem _
id └───────────┘ ┴ ┴ └─────┘
src └───────────┘ ┴ └─────┘
typ └───────────┘ ┴ ┴ └─────┘
741
742 theorem think_equiv (s : computation α) : think s ~ s :=
id └─────────┘ ┴ └───┘ ┴ ┴ ┴
src └─────────┘ └───┘ ┴
typ └─────────┘ ┴ └───┘ ┴ ┴ ┴
doc └─────────┘ └───┘ ┴
743 λ a, ⟨of_think_mem, think_mem⟩
id ┴ └──────────┘ └───────┘
src └──────────┘ └───────┘
typ ┴ └──────────┘ └───────┘
744
745 theorem thinkN_equiv (s : computation α) (n) : thinkN s n ~ s :=
id └─────────┘ ┴ └────┘ ┴ ┴ ┴ ┴
src └─────────┘ └────┘ ┴
typ └─────────┘ ┴ └────┘ ┴ ┴ ┴ ┴
doc └─────────┘ └────┘ ┴
746 λ a, thinkN_mem n
id ┴ └────────┘ ┴
src └────────┘
typ ┴ └────────┘ ┴
747
748 theorem bind_congr {s1 s2 : computation α} {f1 f2 : α → computation β}
id └─────────┘ ┴ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ └─────────┘ ┴ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
749 (h1 : s1 ~ s2) (h2 : ∀ a, f1 a ~ f2 a) : bind s1 f1 ~ bind s2 f2 :=
id └┘ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ └──┘ └┘ └┘ ┴ └──┘ └┘ └┘
src ┴ ┴ └──┘ ┴ └──┘
typ └┘ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ └──┘ └┘ └┘ ┴ └──┘ └┘ └┘
doc ┴ ┴ └──┘ ┴ └──┘
750 λ b, ⟨λh, let ⟨a, ha, hb⟩ := exists_of_mem_bind h in
id ┴ ┴ └─┘ ┴ └┘ └┘ └────────────────┘ ┴
src └────────────────┘
typ ┴ ┴ └─┘ ┴ └┘ └┘ └────────────────┘ ┴
751 mem_bind ((h1 a).1 ha) ((h2 a b).1 hb),
id └──────┘ └┘ ┴ └┘ ┴ ┴
src └──────┘ ┴ ┴
typ └──────┘ └┘ ┴ └┘ ┴ ┴
752 λh, let ⟨a, ha, hb⟩ := exists_of_mem_bind h in
id ┴ └─┘ ┴ └┘ └┘ └────────────────┘ ┴
src └────────────────┘
typ ┴ └─┘ ┴ └┘ └┘ └────────────────┘ ┴
753 mem_bind ((h1 a).2 ha) ((h2 a b).2 hb)⟩
id └──────┘ └┘ ┴ └┘ ┴ ┴
src └──────┘ ┴ ┴
typ └──────┘ └┘ ┴ └┘ ┴ ┴
754
755 theorem equiv_ret_of_mem {s : computation α} {a} (h : a ∈ s) : s ~ return a :=
id └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴
src └─────────┘ ┴ ┴ └────┘
typ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴
doc └─────────┘ ┴ └────┘
756 equiv_of_mem h (ret_mem _)
id └──────────┘ ┴ └─────┘
src └──────────┘ └─────┘
typ └──────────┘ ┴ └─────┘
757
758 /-- `lift_rel R ca cb` is a generalization of `equiv` to relations other than
759 equality. It asserts that if `ca` terminates with `a`, then `cb` terminates with
760 some `b` such that `R a b`, and if `cb` terminates with `b` then `ca` terminates
761 with some `a` such that `R a b`. -/
762 def lift_rel (R : α → β → Prop) (ca : computation α) (cb : computation β) : Prop :=
id ┴ ┴ └─────────┘ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ ┴ ┴ └─────────┘ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
763 (∀ {a}, a ∈ ca → ∃ {b}, b ∈ cb ∧ R a b) ∧
id ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
764 ∀ {b}, b ∈ cb → ∃ {a}, a ∈ ca ∧ R a b
id ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
765
766 theorem lift_rel.swap (R : α → β → Prop) (ca : computation α) (cb : computation β) :
id ┴ ┴ └─────────┘ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ ┴ ┴ └─────────┘ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
767 lift_rel (function.swap R) cb ca ↔ lift_rel R ca cb :=
id └──────┘ └───────────┘ ┴ └┘ └┘ ┴ └──────┘ ┴ └┘ └┘
src └──────┘ └───────────┘ ┴ └──────┘
typ └──────┘ └───────────┘ ┴ └┘ └┘ ┴ └──────┘ ┴ └┘ └┘
doc └──────┘ └──────┘
768 and_comm _ _
id └──────┘
src └──────┘
typ └──────┘
769
770 theorem lift_eq_iff_equiv (c₁ c₂ : computation α) : lift_rel (=) c₁ c₂ ↔ c₁ ~ c₂ :=
id └─────────┘ ┴ └──────┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘
src └─────────┘ └──────┘ ┴ ┴ ┴
typ └─────────┘ ┴ └──────┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘
doc └─────────┘ └──────┘ ┴
771 ⟨λ⟨h1, h2⟩ a,
id ┴└┘ └┘ ┴
typ ┴└┘ └┘ ┴
772 ⟨λ a1, let ⟨b, b2, ab⟩ := h1 a1 in by rwa ab,
id └┘ └─┘ └┘ └┘
src └──┘
typ └┘ └─┘ └┘ └──┘└┘
doc └──┘
txt └──┘
par └──┘
pid ┴
st └─────┘
773 λ a2, let ⟨b, b1, ab⟩ := h2 a2 in by rwa ←ab⟩,
id └┘ └─┘ └┘ └┘
src └───┘
typ └┘ └─┘ └┘ └───┘└┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st └──────┘
774 λe, ⟨λ a a1, ⟨a, (e _).1 a1, rfl⟩, λ a a2, ⟨a, (e _).2 a2, rfl⟩⟩⟩
id ┴ ┴ └┘ ┴ ┴ ┴ └┘ └─┘ ┴ └┘ ┴ ┴ ┴ └┘ └─┘
src ┴ └─┘ ┴ └─┘
typ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └─┘ ┴ └┘ ┴ ┴ ┴ └┘ └─┘
775
776 theorem lift_rel.refl (R : α → α → Prop) (H : reflexive R) : reflexive (lift_rel R) :=
id ┴ ┴ └───────┘ ┴ └───────┘ └──────┘ ┴
src └───────┘ └───────┘ └──────┘
typ ┴ ┴ └───────┘ ┴ └───────┘ └──────┘ ┴
doc └──────┘
777 λ s, ⟨λ a as, ⟨a, as, H a⟩, λ b bs, ⟨b, bs, H b⟩⟩
id ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴
typ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴
778
779 theorem lift_rel.symm (R : α → α → Prop) (H : symmetric R) : symmetric (lift_rel R) :=
id ┴ ┴ └───────┘ ┴ └───────┘ └──────┘ ┴
src └───────┘ └───────┘ └──────┘
typ ┴ ┴ └───────┘ ┴ └───────┘ └──────┘ ┴
doc └──────┘
780 λ s1 s2 ⟨l, r⟩,
id └┘ └┘ ┴┴ ┴
typ └┘ └┘ ┴┴ ┴
781 ⟨λ a a2, let ⟨b, b1, ab⟩ := r a2 in ⟨b, b1, H ab⟩,
id ┴ └┘ └─┘ ┴ └┘ └┘ └┘ ┴
typ ┴ └┘ └─┘ ┴ └┘ └┘ └┘ ┴
782 λ a a1, let ⟨b, b2, ab⟩ := l a1 in ⟨b, b2, H ab⟩⟩
id ┴ └┘ └─┘ ┴ └┘ └┘ └┘ ┴
typ ┴ └┘ └─┘ ┴ └┘ └┘ └┘ ┴
783
784 theorem lift_rel.trans (R : α → α → Prop) (H : transitive R) : transitive (lift_rel R) :=
id ┴ ┴ └────────┘ ┴ └────────┘ └──────┘ ┴
src └────────┘ └────────┘ └──────┘
typ ┴ ┴ └────────┘ ┴ └────────┘ └──────┘ ┴
doc └──────┘
785 λ s1 s2 s3 ⟨l1, r1⟩ ⟨l2, r2⟩,
id └┘ └┘ └┘ ┴└┘ └┘ ┴└┘ └┘
typ └┘ └┘ └┘ ┴└┘ └┘ ┴└┘ └┘
786 ⟨λ a a1, let ⟨b, b2, ab⟩ := l1 a1, ⟨c, c3, bc⟩ := l2 b2 in ⟨c, c3, H ab bc⟩,
id ┴ └┘ └─┘ └┘ └┘ └┘ ┴ └┘ └┘ ┴
typ ┴ └┘ └─┘ └┘ └┘ └┘ ┴ └┘ └┘ ┴
787 λ c c3, let ⟨b, b2, bc⟩ := r2 c3, ⟨a, a1, ab⟩ := r1 b2 in ⟨a, a1, H ab bc⟩⟩
id ┴ └┘ └─┘ └┘ └┘ └┘ ┴ └┘ └┘ ┴
typ ┴ └┘ └─┘ └┘ └┘ └┘ ┴ └┘ └┘ ┴
788
789 theorem lift_rel.equiv (R : α → α → Prop) : equivalence R → equivalence (lift_rel R)
id ┴ ┴ └─────────┘ ┴ ┴ └─────────┘ └──────┘ ┴
src └─────────┘ └─────────┘ └──────┘
typ ┴ ┴ └─────────┘ ┴ ┴ └─────────┘ └──────┘ ┴
doc └──────┘
790 | ⟨refl, symm, trans⟩ :=
id └──┘ └──┘ └───┘
src └──┘ └──┘ └───┘
typ └──┘ └──┘ └───┘
791 ⟨lift_rel.refl R refl, lift_rel.symm R symm, lift_rel.trans R trans⟩
id └───────────┘ ┴ └───────────┘ ┴ └────────────┘ ┴
src └───────────┘ └───────────┘ └────────────┘
typ └───────────┘ ┴ └───────────┘ ┴ └────────────┘ ┴
792
793 theorem lift_rel.imp {R S : α → β → Prop} (H : ∀ {a b}, R a b → S a b) (s t) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
794 lift_rel R s t → lift_rel S s t | ⟨l, r⟩ :=
id └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
src └──────┘ └──────┘
typ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
doc └──────┘ └──────┘
795 ⟨λ a as, let ⟨b, bt, ab⟩ := l as in ⟨b, bt, H ab⟩,
id ┴ └┘ └─┘ ┴ └┘ └┘ └┘ ┴
typ ┴ └┘ └─┘ ┴ └┘ └┘ └┘ ┴
796 λ b bt, let ⟨a, as, ab⟩ := r bt in ⟨a, as, H ab⟩⟩
id ┴ └┘ └─┘ ┴ └┘ └┘ └┘ ┴
typ ┴ └┘ └─┘ ┴ └┘ └┘ └┘ ┴
797
798 theorem terminates_of_lift_rel {R : α → β → Prop} {s t} :
id ┴ ┴
typ ┴ ┴
799 lift_rel R s t → (terminates s ↔ terminates t) | ⟨l, r⟩ :=
id └──────┘ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ └────────┘ ┴ ┴ ┴
src └──────┘ └────────┘ ┴ └────────┘
typ └──────┘ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ └────────┘ ┴ ┴ ┴
doc └──────┘ └────────┘ └────────┘
800 ⟨λ ⟨a, as⟩, let ⟨b, bt, ab⟩ := l as in ⟨b, bt⟩,
id ┴ └┘ └─┘ ┴ └┘
typ ┴ └┘ └─┘ ┴ └┘
801 λ ⟨b, bt⟩, let ⟨a, as, ab⟩ := r bt in ⟨a, as⟩⟩
id ┴ └┘ └─┘ ┴ └┘
typ ┴ └┘ └─┘ ┴ └┘
802
803 theorem rel_of_lift_rel {R : α → β → Prop} {ca cb} :
id ┴ ┴
typ ┴ ┴
804 lift_rel R ca cb → ∀ {a b}, a ∈ ca → b ∈ cb → R a b
id └──────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └──────┘ ┴ ┴
typ └──────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └──────┘
805 | ⟨l, r⟩ a b ma mb :=
id ┴ └┘
typ ┴ └┘
806 let ⟨b', mb', ab'⟩ := l ma in by rw mem_unique mb mb'; exact ab'
id └─┘ └────────┘ └┘ └─┘ └─┘
src └─┘└────────┘┴ ┴ └────┘ └
typ └─┘ └─┘└────────┘┴└┘┴└─┘ └────┘└─┘└
doc └─┘ ┴ ┴ └────┘ └
txt └─┘ ┴ ┴ └────┘ └
par └─┘ ┴ ┴ └────┘ └
pid ┴ ┴ ┴ ┴ └
st └────────────────────────────────
807
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
808 theorem lift_rel_of_mem {R : α → β → Prop} {a b ca cb}
id ┴ ┴
typ ┴ ┴
809 (ma : a ∈ ca) (mb : b ∈ cb) (ab : R a b) : lift_rel R ca cb :=
id ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └──────┘ ┴ └┘ └┘
src ┴ ┴ └──────┘
typ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └──────┘ ┴ └┘ └┘
doc └──────┘
810 ⟨λ a' ma', by rw mem_unique ma' ma; exact ⟨b, mb, ab⟩,
id └┘ └─┘ └────────┘ └─┘ └┘ ┴ └┘ └┘
src └─┘└────────┘┴ ┴ └────┘ └┘ └┘ ┴
typ └┘ └─┘ └─┘└────────┘┴└─┘┴└┘ └────┘ ┴└┘└┘└┘└┘┴
doc └─┘ ┴ ┴ └────┘ └┘ └┘ ┴
txt └─┘ ┴ ┴ └────┘ └┘ └┘ ┴
par └─┘ ┴ ┴ └────┘ └┘ └┘ ┴
pid ┴ ┴ ┴ ┴ └┘ └┘ ┴
st └──────────────────────────────────────┘
811 λ b' mb', by rw mem_unique mb' mb; exact ⟨a, ma, ab⟩⟩
id └┘ └─┘ └────────┘ └─┘ └┘ ┴ └┘ └┘
src └─┘└────────┘┴ ┴ └────┘ └┘ └┘ ┴
typ └┘ └─┘ └─┘└────────┘┴└─┘┴└┘ └────┘ ┴└┘└┘└┘└┘┴
doc └─┘ ┴ ┴ └────┘ └┘ └┘ ┴
txt └─┘ ┴ ┴ └────┘ └┘ └┘ ┴
par └─┘ ┴ ┴ └────┘ └┘ └┘ ┴
pid ┴ ┴ ┴ ┴ └┘ └┘ ┴
st └──────────────────────────────────────┘
812
813 theorem exists_of_lift_rel_left {R : α → β → Prop} {ca cb}
id ┴ ┴
typ ┴ ┴
814 (H : lift_rel R ca cb) {a} (h : a ∈ ca) : ∃ {b}, b ∈ cb ∧ R a b :=
id └──────┘ ┴ └┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
src └──────┘ ┴ ┴ ┴ ┴ ┴
typ └──────┘ ┴ └┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
doc └──────┘
815 H.left h
id ┴└───┘ ┴
src └───┘
typ ┴└───┘ ┴
816
817 theorem exists_of_lift_rel_right {R : α → β → Prop} {ca cb}
id ┴ ┴
typ ┴ ┴
818 (H : lift_rel R ca cb) {b} (h : b ∈ cb) : ∃ {a}, a ∈ ca ∧ R a b :=
id └──────┘ ┴ └┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
src └──────┘ ┴ ┴ ┴ ┴ ┴
typ └──────┘ ┴ └┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
doc └──────┘
819 H.right h
id ┴└────┘ ┴
src └────┘
typ ┴└────┘ ┴
820
821 theorem lift_rel_def {R : α → β → Prop} {ca cb} : lift_rel R ca cb ↔
id ┴ ┴ └──────┘ ┴ └┘ └┘ ┴
src └──────┘ ┴
typ ┴ ┴ └──────┘ ┴ └┘ └┘ ┴
doc └──────┘
822 (terminates ca ↔ terminates cb) ∧ ∀ {a b}, a ∈ ca → b ∈ cb → R a b :=
id └────────┘ └┘ ┴ └────────┘ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └────────┘ ┴ └────────┘ ┴ ┴ ┴
typ └────────┘ └┘ ┴ └────────┘ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └────────┘ └────────┘
823 ⟨λh, ⟨terminates_of_lift_rel h, λ a b ma mb,
id ┴ └────────────────────┘ ┴ ┴ ┴ └┘ └┘
src └────────────────────┘
typ ┴ └────────────────────┘ ┴ ┴ ┴ └┘ └┘
824 let ⟨b', mb', ab⟩ := h.left ma in by rwa mem_unique mb mb'⟩,
id └─┘ ┴└───┘ └┘ └────────┘ └┘ └─┘
src └───┘ └──┘└────────┘┴ ┴
typ └─┘ ┴└───┘ └┘ └──┘└────────┘┴└┘┴└─┘
doc └──┘ ┴ ┴
txt └──┘ ┴ ┴
par └──┘ ┴ ┴
pid ┴ ┴ ┴
st └────────────────────┘
825 λ⟨l, r⟩,
id ┴┴ ┴
typ ┴┴ ┴
826 ⟨λ a ma, let ⟨b, mb⟩ := l.1 ⟨_, ma⟩ in ⟨b, mb, r ma mb⟩,
id ┴ └┘ └─┘ ┴ └┘ ┴ └┘ └┘
src ┴
typ ┴ └┘ └─┘ ┴ └┘ ┴ └┘ └┘
827 λ b mb, let ⟨a, ma⟩ := l.2 ⟨_, mb⟩ in ⟨a, ma, r ma mb⟩⟩⟩
id ┴ └┘ └─┘ ┴ └┘ ┴ └┘ └┘
src ┴
typ ┴ └┘ └─┘ ┴ └┘ ┴ └┘ └┘
828
829 theorem lift_rel_bind {δ} (R : α → β → Prop) (S : γ → δ → Prop)
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
830 {s1 : computation α} {s2 : computation β}
id └─────────┘ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ └─────────┘ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
831 {f1 : α → computation γ} {f2 : β → computation δ}
id ┴ └─────────┘ ┴ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ ┴ └─────────┘ ┴ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
832 (h1 : lift_rel R s1 s2) (h2 : ∀ {a b}, R a b → lift_rel S (f1 a) (f2 b))
id └──────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ └┘ ┴ └┘ ┴
src └──────┘ └──────┘
typ └──────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ └┘ ┴ └┘ ┴
doc └──────┘ └──────┘
833 : lift_rel S (bind s1 f1) (bind s2 f2) :=
id └──────┘ ┴ └──┘ └┘ └┘ └──┘ └┘ └┘
src └──────┘ └──┘ └──┘
typ └──────┘ ┴ └──┘ └┘ └┘ └──┘ └┘ └┘
doc └──────┘ └──┘ └──┘
834 let ⟨l1, r1⟩ := h1 in
id └─┘ └┘ └┘ └┘
typ └─┘ └┘ └┘ └┘
835 ⟨λ c cB,
id ┴ └┘
typ ┴ └┘
836 let ⟨a, a1, c₁⟩ := exists_of_mem_bind cB,
id └─┘ └┘ └┘ └────────────────┘ └┘
src └────────────────┘
typ └─┘ └┘ └┘ └────────────────┘ └┘
837 ⟨b, b2, ab⟩ := l1 a1,
id └┘ └┘
typ └┘ └┘
838 ⟨l2, r2⟩ := h2 ab,
id └┘ └┘
typ └┘ └┘
839 ⟨d, d2, cd⟩ := l2 c₁ in
id └┘ └┘
typ └┘ └┘
840 ⟨_, mem_bind b2 d2, cd⟩,
id └──────┘
src └──────┘
typ └──────┘
841 λ d dB,
id ┴ └┘
typ ┴ └┘
842 let ⟨b, b1, d1⟩ := exists_of_mem_bind dB,
id └─┘ └┘ └┘ └────────────────┘ └┘
src └────────────────┘
typ └─┘ └┘ └┘ └────────────────┘ └┘
843 ⟨a, a2, ab⟩ := r1 b1,
id └┘ └┘
typ └┘ └┘
844 ⟨l2, r2⟩ := h2 ab,
id └┘ └┘
typ └┘ └┘
845 ⟨c, c₂, cd⟩ := r2 d1 in
id └┘ └┘
typ └┘ └┘
846 ⟨_, mem_bind a2 c₂, cd⟩⟩
id └──────┘
src └──────┘
typ └──────┘
847
848 @[simp] theorem lift_rel_return_left (R : α → β → Prop) (a : α) (cb : computation β) :
id ┴ ┴ ┴ └─────────┘ ┴
src └─────────┘
typ ┴ ┴ ┴ └─────────┘ ┴
doc └──┘ └─────────┘
849 lift_rel R (return a) cb ↔ ∃ {b}, b ∈ cb ∧ R a b :=
id └──────┘ ┴ └────┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
src └──────┘ └────┘ ┴ ┴ ┴ ┴ ┴
typ └──────┘ ┴ └────┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
doc └──────┘ └────┘
850 ⟨λ⟨l, r⟩, l (ret_mem _),
id ┴┴ └─────┘
src └─────┘
typ ┴┴ └─────┘
851 λ⟨b, mb, ab⟩,
id ┴
typ ┴
852 ⟨λ a' ma', by rw eq_of_ret_mem ma'; exact ⟨b, mb, ab⟩,
id └┘ └─┘ └───────────┘ └─┘ ┴ └┘ └┘
src └─┘└───────────┘┴ └────┘ └┘ └┘ ┴
typ └┘ └─┘ └─┘└───────────┘┴└─┘ └────┘ ┴└┘└┘└┘└┘┴
doc └─┘ ┴ └────┘ └┘ └┘ ┴
txt └─┘ ┴ └────┘ └┘ └┘ ┴
par └─┘ ┴ └────┘ └┘ └┘ ┴
pid ┴ ┴ ┴ └┘ └┘ ┴
st └──────────────────────────────────────┘
853 λ b' mb', ⟨_, ret_mem _, by rw mem_unique mb' mb; exact ab⟩⟩⟩
id └┘ └─┘ └─────┘ └────────┘ └─┘ └┘ └┘
src └─────┘ └─┘└────────┘┴ ┴ └────┘
typ └┘ └─┘ └─────┘ └─┘└────────┘┴└─┘┴└┘ └────┘└┘
doc └─┘ ┴ ┴ └────┘
txt └─┘ ┴ ┴ └────┘
par └─┘ ┴ ┴ └────┘
pid ┴ ┴ ┴ ┴
st └─────────────────────────────┘
854
855 @[simp] theorem lift_rel_return_right (R : α → β → Prop) (ca : computation α) (b : β) :
id ┴ ┴ └─────────┘ ┴ ┴
src └─────────┘
typ ┴ ┴ └─────────┘ ┴ ┴
doc └──┘ └─────────┘
856 lift_rel R ca (return b) ↔ ∃ {a}, a ∈ ca ∧ R a b :=
id └──────┘ ┴ └┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
src └──────┘ └────┘ ┴ ┴ ┴ ┴ ┴
typ └──────┘ ┴ └┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
doc └──────┘ └────┘
857 by rw [lift_rel.swap, lift_rel_return_left]
id └───────────┘ └──────────────────┘
src └──┘└───────────┘└┘└──────────────────┘└─
typ └──┘└───────────┘└┘└──────────────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └────────────────┘└────────────────────┘┴└
858
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
859 @[simp] theorem lift_rel_return (R : α → β → Prop) (a : α) (b : β) :
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
doc └──┘
860 lift_rel R (return a) (return b) ↔ R a b :=
id └──────┘ ┴ └────┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
src └──────┘ └────┘ └────┘ ┴
typ └──────┘ ┴ └────┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
doc └──────┘ └────┘ └────┘
861 by rw [lift_rel_return_left]; exact
id └──────────────────┘
src └──┘└──────────────────┘┴ └────┘
typ └──┘└──────────────────┘┴ └────┘
doc └──┘ ┴ └────┘
txt └──┘ ┴ └────┘
par └──┘ ┴ └────┘
pid └┘ ┴ ┴
st └───────────────────────┘┴└───────
862 ⟨λ⟨b', mb', ab'⟩, by rwa eq_of_ret_mem mb' at ab',
id └───────────┘ └─┘
src ┴ └┘ └┘ └─┘ ┴└──┘└───────────┘┴ └─────┘└─
typ ┴ └┘ └┘ └─┘ ┴└──┘└───────────┘┴└─┘└─────┘└─
doc ┴ └┘ └┘ └─┘ ┴└──┘ ┴ └─────┘└─
txt ┴ └┘ └┘ └─┘ ┴└──┘ ┴ └─────┘└─
par ┴ └┘ └┘ └─┘ ┴└──┘ ┴ └─────┘└─
pid ┴ └┘ └┘ └─┘ └───┘ ┴ └────────
st ───────────────────┘└───────────────────────────┘└─
863 λab, ⟨_, ret_mem _, ab⟩⟩
id └─────┘
src ┘ └──┘ └─┘└─────┘└──┘ └──
typ ┘ └──┘ └─┘└─────┘└──┘ └──
doc ┘ └──┘ └─┘ └──┘ └──
txt ┘ └──┘ └─┘ └──┘ └──
par ┘ └──┘ └─┘ └──┘ └──
pid ┘ └──┘ └─┘ └──┘ └┘└
st ──────────────────────────
864
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
865 @[simp] theorem lift_rel_think_left (R : α → β → Prop) (ca : computation α) (cb : computation β) :
id ┴ ┴ └─────────┘ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ ┴ ┴ └─────────┘ ┴ └─────────┘ ┴
doc └──┘ └─────────┘ └─────────┘
866 lift_rel R (think ca) cb ↔ lift_rel R ca cb :=
id └──────┘ ┴ └───┘ └┘ └┘ ┴ └──────┘ ┴ └┘ └┘
src └──────┘ └───┘ ┴ └──────┘
typ └──────┘ ┴ └───┘ └┘ └┘ ┴ └──────┘ ┴ └┘ └┘
doc └──────┘ └───┘ └──────┘
867 and_congr (forall_congr $ λb, imp_congr ⟨of_think_mem, think_mem⟩ iff.rfl)
id └───────┘ └──────────┘ ┴ └───────┘ └──────────┘ └───────┘ └─────┘
src └───────┘ └──────────┘ └───────┘ └──────────┘ └───────┘ └─────┘
typ └───────┘ └──────────┘ ┴ └───────┘ └──────────┘ └───────┘ └─────┘
868 (forall_congr $ λb, imp_congr iff.rfl $
id └──────────┘ ┴ └───────┘ └─────┘
src └──────────┘ └───────┘ └─────┘
typ └──────────┘ ┴ └───────┘ └─────┘
869 exists_congr $ λ b, and_congr ⟨of_think_mem, think_mem⟩ iff.rfl)
id └──────────┘ ┴ └───────┘ └──────────┘ └───────┘ └─────┘
src └──────────┘ └───────┘ └──────────┘ └───────┘ └─────┘
typ └──────────┘ ┴ └───────┘ └──────────┘ └───────┘ └─────┘
870
871 @[simp] theorem lift_rel_think_right (R : α → β → Prop) (ca : computation α) (cb : computation β) :
id ┴ ┴ └─────────┘ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ ┴ ┴ └─────────┘ ┴ └─────────┘ ┴
doc └──┘ └─────────┘ └─────────┘
872 lift_rel R ca (think cb) ↔ lift_rel R ca cb :=
id └──────┘ ┴ └┘ └───┘ └┘ ┴ └──────┘ ┴ └┘ └┘
src └──────┘ └───┘ ┴ └──────┘
typ └──────┘ ┴ └┘ └───┘ └┘ ┴ └──────┘ ┴ └┘ └┘
doc └──────┘ └───┘ └──────┘
873 by rw [←lift_rel.swap R, ←lift_rel.swap R]; apply lift_rel_think_left
id └───────────┘ ┴ └───────────┘ ┴ └─────────────────┘
src └───┘└───────────┘┴ └─┘└───────────┘┴ ┴ └────┘└─────────────────┘└
typ └───┘└───────────┘┴┴└─┘└───────────┘┴┴┴ └────┘└─────────────────┘└
doc └───┘ ┴ └─┘ ┴ ┴ └────┘ └
txt └───┘ ┴ └─┘ ┴ ┴ └────┘ └
par └───┘ ┴ └─┘ ┴ ┴ └────┘ └
pid └─┘ ┴ └─┘ ┴ ┴ ┴ └
st └───────────────────┘└────────────────┘┴└───────────────────────────
874
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
875 theorem lift_rel_mem_cases {R : α → β → Prop} {ca cb}
id ┴ ┴
typ ┴ ┴
876 (Ha : ∀ a ∈ ca, lift_rel R ca cb)
id ┴ └┘ └──────┘ ┴ └┘ └┘
src ┴ └──────┘
typ ┴ └┘ └──────┘ ┴ └┘ └┘
doc └──────┘
877 (Hb : ∀ b ∈ cb, lift_rel R ca cb) : lift_rel R ca cb :=
id ┴ └┘ └──────┘ ┴ └┘ └┘ └──────┘ ┴ └┘ └┘
src └──────┘ └──────┘
typ ┴ └┘ └──────┘ ┴ └┘ └┘ └──────┘ ┴ └┘ └┘
doc └──────┘ └──────┘
878 ⟨λ a ma, (Ha _ ma).left ma, λ b mb, (Hb _ mb).right mb⟩
id ┴ └┘ └┘ └┘ └──┘ └┘ ┴ └┘ └┘ └┘ └───┘ └┘
src └──┘ └───┘
typ ┴ └┘ └┘ └┘ └──┘ └┘ ┴ └┘ └┘ └┘ └───┘ └┘
879
880 theorem lift_rel_congr {R : α → β → Prop} {ca ca' : computation α} {cb cb' : computation β}
id ┴ ┴ └─────────┘ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ ┴ ┴ └─────────┘ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
881 (ha : ca ~ ca') (hb : cb ~ cb') : lift_rel R ca cb ↔ lift_rel R ca' cb' :=
id └┘ ┴ └─┘ └┘ ┴ └─┘ └──────┘ ┴ └┘ └┘ ┴ └──────┘ ┴ └─┘ └─┘
src ┴ ┴ └──────┘ ┴ └──────┘
typ └┘ ┴ └─┘ └┘ ┴ └─┘ └──────┘ ┴ └┘ └┘ ┴ └──────┘ ┴ └─┘ └─┘
doc ┴ ┴ └──────┘ └──────┘
882 and_congr
id └───────┘
src └───────┘
typ └───────┘
883 (forall_congr $ λ a, imp_congr (ha _) $ exists_congr $ λ b, and_congr (hb _) iff.rfl)
id └──────────┘ ┴ └───────┘ └┘ └──────────┘ ┴ └───────┘ └┘ └─────┘
src └──────────┘ └───────┘ └──────────┘ └───────┘ └─────┘
typ └──────────┘ ┴ └───────┘ └┘ └──────────┘ ┴ └───────┘ └┘ └─────┘
884 (forall_congr $ λ b, imp_congr (hb _) $ exists_congr $ λ a, and_congr (ha _) iff.rfl)
id └──────────┘ ┴ └───────┘ └┘ └──────────┘ ┴ └───────┘ └┘ └─────┘
src └──────────┘ └───────┘ └──────────┘ └───────┘ └─────┘
typ └──────────┘ ┴ └───────┘ └┘ └──────────┘ ┴ └───────┘ └┘ └─────┘
885
886 theorem lift_rel_map {δ} (R : α → β → Prop) (S : γ → δ → Prop)
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
887 {s1 : computation α} {s2 : computation β}
id └─────────┘ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ └─────────┘ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
888 {f1 : α → γ} {f2 : β → δ}
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
889 (h1 : lift_rel R s1 s2) (h2 : ∀ {a b}, R a b → S (f1 a) (f2 b))
id └──────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴
src └──────┘
typ └──────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴
doc └──────┘
890 : lift_rel S (map f1 s1) (map f2 s2) :=
id └──────┘ ┴ └─┘ └┘ └┘ └─┘ └┘ └┘
src └──────┘ └─┘ └─┘
typ └──────┘ ┴ └─┘ └┘ └┘ └─┘ └┘ └┘
doc └──────┘ └─┘ └─┘
891 by rw [←bind_ret, ←bind_ret]; apply lift_rel_bind _ _ h1; simp; exact @h2
id └──────┘ └──────┘ └───────────┘ └┘ └┘
src └───┘└──────┘└─┘└──────┘┴ └────┘└───────────┘└───┘ └──┘ └────┘ └
typ └───┘└──────┘└─┘└──────┘┴ └────┘└───────────┘└───┘└┘ └──┘ └────┘ └┘└
doc └───┘ └─┘ ┴ └────┘ └───┘ └──┘ └────┘ └
txt └───┘ └─┘ ┴ └────┘ └───┘ └──┘ └────┘ └
par └───┘ └─┘ ┴ └────┘ └───┘ └──┘ └────┘ └
pid └─┘ └─┘ ┴ ┴ └───┘ ┴ └
st └────────────┘└─────────┘┴└─────────────────────────────────────────────
892
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
893 theorem map_congr (R : α → α → Prop) (S : β → β → Prop)
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
894 {s1 s2 : computation α} {f : α → β}
id └─────────┘ ┴ ┴ ┴
src └─────────┘
typ └─────────┘ ┴ ┴ ┴
doc └─────────┘
895 (h1 : s1 ~ s2) : map f s1 ~ map f s2 :=
id └┘ ┴ └┘ └─┘ ┴ └┘ ┴ └─┘ ┴ └┘
src ┴ └─┘ ┴ └─┘
typ └┘ ┴ └┘ └─┘ ┴ └┘ ┴ └─┘ ┴ └┘
doc ┴ └─┘ ┴ └─┘
896 by rw [←lift_eq_iff_equiv];
id └───────────────┘
src └───┘└───────────────┘┴
typ └───┘└───────────────┘┴
doc └───┘ ┴
txt └───┘ ┴
par └───┘ ┴
pid └─┘ ┴
st └─────────────────────┘┴└─
897 exact lift_rel_map eq _ ((lift_eq_iff_equiv _ _).2 h1) (λ a b, congr_arg _)
id └──────────┘ └┘ └───────────────┘ └┘ └───────┘
src └────┘└──────────┘┴└┘└─┘ └───────────────┘└──────┘ └┘ └────┘└───────┘└───
typ └────┘└──────────┘┴└┘└─┘ └───────────────┘└──────┘└┘└┘ └────┘└───────┘└───
doc └────┘ ┴ └─┘ └──────┘ └┘ └────┘ └───
txt └────┘ ┴ └─┘ └──────┘ └┘ └────┘ └───
par └────┘ ┴ └─┘ └──────┘ └┘ └────┘ └───
pid ┴ ┴ └─┘ └──────┘ └┘ └────┘ └─┘└
st ───────────────────────────────────────────────────────────────────────────────
898
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
899 def lift_rel_aux (R : α → β → Prop)
id ┴ ┴
typ ┴ ┴
900 (C : computation α → computation β → Prop) :
id └─────────┘ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ └─────────┘ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
901 α ⊕ computation α → β ⊕ computation β → Prop
id ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ └─────────┘ ┴
src ┴ └─────────┘ ┴ └─────────┘
typ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
902 | (sum.inl a) (sum.inl b) := R a b
id ┴ └─────┘ ┴ ┴
src └─────┘
typ ┴ └─────┘ ┴ ┴
903 | (sum.inl a) (sum.inr cb) := ∃ {b}, b ∈ cb ∧ R a b
id └─────┘ ┴ └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ └─────┘ ┴ ┴ ┴ ┴
typ └─────┘ ┴ └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
904 | (sum.inr ca) (sum.inl b) := ∃ {a}, a ∈ ca ∧ R a b
id └─────┘ └┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ └─────┘ ┴ ┴ ┴ ┴
typ └─────┘ └┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
905 | (sum.inr ca) (sum.inr cb) := C ca cb
id └┘ └─────┘ └┘ ┴
src └─────┘
typ └┘ └─────┘ └┘ ┴
906 attribute [simp] lift_rel_aux
id └──────────┘
src └──────────┘
typ └──────────┘
doc └──┘
907
908 @[simp] lemma lift_rel_aux.ret_left (R : α → β → Prop)
id ┴ ┴
typ ┴ ┴
doc └──┘
909 (C : computation α → computation β → Prop) (a cb) :
id └─────────┘ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ └─────────┘ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
910 lift_rel_aux R C (sum.inl a) (destruct cb) ↔ ∃ {b}, b ∈ cb ∧ R a b :=
id └──────────┘ ┴ ┴ └─────┘ ┴ └──────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
src └──────────┘ └─────┘ └──────┘ ┴ ┴ ┴ ┴ ┴
typ └──────────┘ ┴ ┴ └─────┘ ┴ └──────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
doc └──────┘
911 begin
st └─────
912 apply cb.cases_on (λ b, _) (λ cb, _),
id └─────────┘
src └────┘└─────────┘┴ └─────┘ └─────┘
typ └────┘└─────────┘┴ └─────┘ └─────┘
doc └────┘ ┴ └─────┘ └─────┘
txt └────┘ ┴ └─────┘ └─────┘
par └────┘ ┴ └─────┘ └─────┘
pid ┴ ┴ └─────┘ └─────┘
st ─────────────────────────────────────┘└─
913 { exact ⟨λ h, ⟨_, ret_mem _, h⟩, λ ⟨b', mb, h⟩,
id └─────┘
src └────┘ └──┘ └─┘└─────┘└──┘ └─┘ └┘ └┘ └┘ └──
typ └────┘ └──┘ └─┘└─────┘└──┘ └─┘ └┘ └┘ └┘ └──
doc └────┘ └──┘ └─┘ └──┘ └─┘ └┘ └┘ └┘ └──
txt └────┘ └──┘ └─┘ └──┘ └─┘ └┘ └┘ └┘ └──
par └────┘ └──┘ └─┘ └──┘ └─┘ └┘ └┘ └┘ └──
pid ┴ └──┘ └─┘ └──┘ └─┘ └┘ └┘ └┘ └──
st ───┘└─────────────────────────────────────────────
914 by rw [mem_unique (ret_mem _) mb]; exact h⟩ },
id └────────┘ └─────┘ └┘ ┴
src ───┘ ┴└──┘└────────┘┴ └─────┘└──┘ ┴└──────┘ └┘
typ ───┘ ┴└──┘└────────┘┴ └─────┘└──┘└┘┴└──────┘┴└┘
doc ───┘ ┴└──┘ ┴ └──┘ ┴└──────┘ └┘
txt ───┘ ┴└──┘ ┴ └──┘ ┴└──────┘ └┘
par ───┘ ┴└──┘ ┴ └──┘ ┴└──────┘ └┘
pid ───┘ └───┘ ┴ └──┘ └───────┘ ┴┴
st ─────┘└────────────────────────────┘┴└───────┘└┘└┘└
915 { rw [destruct_think],
id └────────────┘
src └──┘└────────────┘┴
typ └──┘└────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ─────────────────────┘└──
916 exact ⟨λ ⟨b, h, r⟩, ⟨b, think_mem h, r⟩,
id ┴ ┴ ┴ └───────┘
src └────┘ └┘ └┘ └┘ └─┘ └┘└───────┘┴ └┘ └──
typ └────┘ └┘┴└┘┴└┘┴└─┘ └┘└───────┘┴ └┘ └──
doc └────┘ └┘ └┘ └┘ └─┘ └┘ ┴ └┘ └──
txt └────┘ └┘ └┘ └┘ └─┘ └┘ ┴ └┘ └──
par └────┘ └┘ └┘ └┘ └─┘ └┘ ┴ └┘ └──
pid ┴ └┘ └┘ └┘ └─┘ └┘ ┴ └┘ └──
st ─────────────────────────────────────────────
917 λ ⟨b, h, r⟩, ⟨b, of_think_mem h, r⟩⟩ }
id ┴ ┴ ┴ └──────────┘
src ──────────┘ └┘ └┘ └┘ └─┘ └┘└──────────┘┴ └┘ └─┘
typ ──────────┘ └┘┴└┘┴└┘┴└─┘ └┘└──────────┘┴ └┘ └─┘
doc ──────────┘ └┘ └┘ └┘ └─┘ └┘ ┴ └┘ └─┘
txt ──────────┘ └┘ └┘ └┘ └─┘ └┘ ┴ └┘ └─┘
par ──────────┘ └┘ └┘ └┘ └─┘ └┘ ┴ └┘ └─┘
pid ──────────┘ └┘ └┘ └┘ └─┘ └┘ ┴ └┘ └┘┴
st ───────────────────────────────────────────────┘└─
918 end
st ──┘
919
920 theorem lift_rel_aux.swap (R : α → β → Prop) (C) (a b) :
id ┴ ┴
typ ┴ ┴
921 lift_rel_aux (function.swap R) (function.swap C) b a = lift_rel_aux R C a b :=
id └──────────┘ └───────────┘ ┴ └───────────┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴
src └──────────┘ └───────────┘ └───────────┘ ┴ └──────────┘
typ └──────────┘ └───────────┘ ┴ └───────────┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴
922 by cases a with a ca; cases b with b cb; simp only [lift_rel_aux]
id ┴ ┴ └──────────┘
src └────┘ └────────┘ └────┘ └────────┘ └─────────┘└──────────┘└─
typ └────┘┴└────────┘ └────┘┴└────────┘ └─────────┘└──────────┘└─
doc └────┘ └────────┘ └────┘ └────────┘ └─────────┘ └─
txt └────┘ └────────┘ └────┘ └────────┘ └─────────┘ └─
par └────┘ └────────┘ └────┘ └────────┘ └─────────┘ └─
pid ┴ └────────┘ ┴ └────────┘ ┴└──┘└┘ ┴└
st └───────────────────────────────────────────────────────────────
923
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
924 @[simp] lemma lift_rel_aux.ret_right (R : α → β → Prop)
id ┴ ┴
typ ┴ ┴
doc └──┘
925 (C : computation α → computation β → Prop) (b ca) :
id └─────────┘ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ └─────────┘ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
926 lift_rel_aux R C (destruct ca) (sum.inl b) ↔ ∃ {a}, a ∈ ca ∧ R a b :=
id └──────────┘ ┴ ┴ └──────┘ └┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
src └──────────┘ └──────┘ └─────┘ ┴ ┴ ┴ ┴ ┴
typ └──────────┘ ┴ ┴ └──────┘ └┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
doc └──────┘
927 by rw [←lift_rel_aux.swap, lift_rel_aux.ret_left]
id └───────────────┘ └───────────────────┘
src └───┘└───────────────┘└┘└───────────────────┘└─
typ └───┘└───────────────┘└┘└───────────────────┘└─
doc └───┘ └┘ └─
txt └───┘ └┘ └─
par └───┘ └┘ └─
pid └─┘ └┘ ┴└
st └─────────────────────┘└─────────────────────┘┴└
928
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
929 theorem lift_rel_rec.lem {R : α → β → Prop} (C : computation α → computation β → Prop)
id ┴ ┴ └─────────┘ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ ┴ ┴ └─────────┘ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
930 (H : ∀ {ca cb}, C ca cb → lift_rel_aux R C (destruct ca) (destruct cb))
id └┘ └┘ ┴ └┘ └┘ └──────────┘ ┴ ┴ └──────┘ └┘ └──────┘ └┘
src └──────────┘ └──────┘ └──────┘
typ └┘ └┘ ┴ └┘ └┘ └──────────┘ ┴ ┴ └──────┘ └┘ └──────┘ └┘
doc └──────┘ └──────┘
931 (ca cb) (Hc : C ca cb) (a) (ha : a ∈ ca) : lift_rel R ca cb :=
id ┴ └┘ └┘ ┴ ┴ └┘ └──────┘ ┴ └┘ └┘
src ┴ └──────┘
typ ┴ └┘ └┘ ┴ ┴ └┘ └──────┘ ┴ └┘ └┘
doc └──────┘
932 begin
st └─────
933 revert cb, refine mem_rec_on ha _ (λ ca' IH, _);
id └────────┘ └┘
src └───────┘ └─────┘└────────┘┴ └─┘ └─────────┘
typ └───────┘ └─────┘└────────┘┴└┘└─┘ └─────────┘
doc └───────┘ └─────┘ ┴ └─┘ └─────────┘
txt └───────┘ └─────┘ ┴ └─┘ └─────────┘
par └───────┘ └─────┘ ┴ └─┘ └─────────┘
pid └─┘ ┴ ┴ └─┘ └─────────┘
st ──────────┘└───────────────────────────────────────
934 intros cb Hc; have h := H Hc,
id ┴ └┘
src └──────────┘ └────────┘ ┴
typ └──────────┘ └────────┘┴┴└┘
doc └──────────┘ └────────┘ ┴
txt └──────────┘ └────────┘ ┴
par └──────────┘ └────────┘ ┴
pid └────┘ └────┘┴└─┘ ┴
st ─────────────────────────────┘└─
935 { simp at h, simp [h] },
id ┴
src └───────┘ └────┘ └┘
typ └───────┘ └────┘┴└┘
doc └───────┘ └────┘ └┘
txt └───────┘ └────┘ └┘
par └───────┘ └────┘ └┘
pid ┴└──┘ ┴┴ ┴┴
st ───┘└───────┘└─────────┘└┘└
936 { have h := H Hc, simp, revert h, apply cb.cases_on (λ b, _) (λ cb', _);
id ┴ └┘ └─────────┘
src └────────┘ ┴ └──┘ └──────┘ └────┘└─────────┘┴ └─────┘ └──────┘
typ └────────┘┴┴└┘ └──┘ └──────┘ └────┘└─────────┘┴ └─────┘ └──────┘
doc └────────┘ ┴ └──┘ └──────┘ └────┘ ┴ └─────┘ └──────┘
txt └────────┘ ┴ └──┘ └──────┘ └────┘ ┴ └─────┘ └──────┘
par └────────┘ ┴ └──┘ └──────┘ └────┘ ┴ └─────┘ └──────┘
pid └────┘┴└─┘ ┴ └┘ ┴ ┴ └─────┘ └──────┘
st ─────────────────┘└────┘└────────┘└────────────────────────────────────────
937 intro h; simp at h; simp [h], exact IH _ h }
id ┴ └┘ ┴
src └─────┘ └───────┘ └────┘ ┴ └────┘ └─┘ ┴
typ └─────┘ └───────┘ └────┘┴┴ └────┘└┘└─┘┴┴
doc └─────┘ └───────┘ └────┘ ┴ └────┘ └─┘ ┴
txt └─────┘ └───────┘ └────┘ ┴ └────┘ └─┘ ┴
par └─────┘ └───────┘ └────┘ ┴ └────┘ └─┘ ┴
pid └┘ ┴└──┘ ┴┴ ┴ ┴ └─┘ ┴
st ───────────────────────────────┘└─────────────┘└─
938 end
st ──┘
939
940 theorem lift_rel_rec {R : α → β → Prop} (C : computation α → computation β → Prop)
id ┴ ┴ └─────────┘ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ ┴ ┴ └─────────┘ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
941 (H : ∀ {ca cb}, C ca cb → lift_rel_aux R C (destruct ca) (destruct cb))
id └┘ └┘ ┴ └┘ └┘ └──────────┘ ┴ ┴ └──────┘ └┘ └──────┘ └┘
src └──────────┘ └──────┘ └──────┘
typ └┘ └┘ ┴ └┘ └┘ └──────────┘ ┴ ┴ └──────┘ └┘ └──────┘ └┘
doc └──────┘ └──────┘
942 (ca cb) (Hc : C ca cb) : lift_rel R ca cb :=
id ┴ └┘ └┘ └──────┘ ┴ └┘ └┘
src └──────┘
typ ┴ └┘ └┘ └──────┘ ┴ └┘ └┘
doc └──────┘
943 lift_rel_mem_cases (lift_rel_rec.lem C @H ca cb Hc) (λ b hb,
id └────────────────┘ └──────────────┘ ┴ ┴ └┘ └┘ └┘ ┴ └┘
src └────────────────┘ └──────────────┘
typ └────────────────┘ └──────────────┘ ┴ ┴ └┘ └┘ └┘ ┴ └┘
944 (lift_rel.swap _ _ _).2 $
id └───────────┘ ┴
src └───────────┘ ┴
typ └───────────┘ ┴
945 lift_rel_rec.lem (function.swap C)
id └──────────────┘ └───────────┘ ┴
src └──────────────┘ └───────────┘
typ └──────────────┘ └───────────┘ ┴
946 (λ cb ca h, cast (lift_rel_aux.swap _ _ _ _).symm $ H h)
id └┘ └┘ ┴ └──┘ └───────────────┘ └──┘ ┴ ┴
src └──┘ └───────────────┘ └──┘
typ └┘ └┘ ┴ └──┘ └───────────────┘ └──┘ ┴ ┴
947 cb ca Hc b hb)
id └┘ └┘ └┘ ┴ └┘
typ └┘ └┘ └┘ ┴ └┘
948
949 end computation